# HG changeset patch
# User wenzelm
# Date 1564646137 -7200
# Node ID 492cb3aaa56281141602d3fba35a48db4e7f5003
# Parent  70019ab5e57fab0a87994fff42be0942026bbe8b
simplified module structure: back to plain datatype (see 95f4f08f950f and 70019ab5e57f);

diff -r 70019ab5e57f -r 492cb3aaa562 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Aug 01 09:50:20 2019 +0200
+++ b/src/Pure/thm.ML	Thu Aug 01 09:55:37 2019 +0200
@@ -164,8 +164,7 @@
 
 (** certified types **)
 
-abstype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: sort Ord_List.T}
-with
+datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: sort Ord_List.T};
 
 fun typ_of (Ctyp {T, ...}) = T;
 
@@ -218,9 +217,8 @@
 (** certified terms **)
 
 (*certified terms with checked typ, maxidx, and sorts*)
-abstype cterm =
-  Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T}
-with
+datatype cterm =
+  Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T};
 
 exception CTERM of string * cterm list;
 
@@ -349,7 +347,7 @@
 
 (*** Derivations and Theorems ***)
 
-abstype thm = Thm of
+datatype thm = Thm of
  deriv *                        (*derivation*)
  {cert: Context.certificate,    (*background theory certificate*)
   tags: Properties.T,           (*additional annotations/comments*)
@@ -360,8 +358,7 @@
   prop: term}                   (*conclusion*)
 and deriv = Deriv of
  {promises: (serial * thm future) Ord_List.T,
-  body: Proofterm.proof_body}
-with
+  body: Proofterm.proof_body};
 
 type conv = cterm -> thm;
 
@@ -1891,10 +1888,6 @@
       end
   end;
 
-end;
-end;
-end;
-
 
 (* authentic derivation names *)