simplified module structure: back to plain datatype (see 95f4f08f950f and 70019ab5e57f);

--- 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 *)