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