From c780b1778e97afe15a0eb2522505b796cd5bbe71 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 20 Feb 2020 13:07:22 -0600
Subject: [PATCH] Minor removals (#3786)

Found while working on parser migration of datatypes.
---
 src/expr/dtype.h                                   |  3 ---
 src/theory/datatypes/theory_datatypes_type_rules.h | 10 ----------
 2 files changed, 13 deletions(-)

diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index b2399472a..08fe9965b 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -243,9 +243,6 @@ class DType
   /** is this a tuple datatype? */
   bool isTuple() const;
 
-  /** get the record representation for this datatype */
-  Record* getRecord() const;
-
   /**
    * Return the cardinality of this datatype.
    * The DType must be resolved.
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index e11ac67f1..0779fdc58 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -24,19 +24,9 @@
 #include "theory/datatypes/theory_datatypes_utils.h"
 
 namespace CVC4 {
-
-namespace expr {
-namespace attr {
-struct DatatypeConstructorTypeGroundTermTag {};
-} /* CVC4::expr::attr namespace */
-} /* CVC4::expr namespace */
-
 namespace theory {
 namespace datatypes {
 
-typedef expr::Attribute<expr::attr::DatatypeConstructorTypeGroundTermTag, Node>
-    GroundTermAttr;
-
 struct DatatypeConstructorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {
-- 
2.30.2