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