src/Pure/thm.ML

   val put_name: string -> thm -> thm
   val extern_oracles: theory -> xstring list
   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
 
-structure Thm:> THM =
+structure Thm: THM =
 struct
 
 structure Pt = Proofterm;
 
 
 (*** Certified terms and types ***)
 
 (** certified types **)
 
-datatype ctyp = Ctyp of
+abstype ctyp = Ctyp of
  {thy_ref: theory_ref,
   T: typ,
   maxidx: int,
-  sorts: sort OrdList.T};
+  sorts: sort OrdList.T}
+with
 
 fun rep_ctyp (Ctyp args) = args;
 fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
 fun typ_of (Ctyp {T, ...}) = T;
 

 
 
 (** certified terms **)
 
 (*certified terms with checked typ, maxidx, and sorts*)
-datatype cterm = Cterm of
+abstype cterm = Cterm of
  {thy_ref: theory_ref,
   t: term,
   T: typ,
   maxidx: int,
-  sorts: sort OrdList.T};
+  sorts: sort OrdList.T}
+with
 
 exception CTERM of string * cterm list;
 
 fun rep_cterm (Cterm args) = args;
 

 
 
 
 (*** Derivations and Theorems ***)
 
-datatype thm = Thm of
+abstype thm = Thm of
  deriv *                                        (*derivation*)
  {thy_ref: theory_ref,                          (*dynamic reference to theory*)
   tags: Properties.T,                           (*additional annotations/comments*)
   maxidx: int,                                  (*maximum index of any Var or TVar*)
   shyps: sort OrdList.T,                        (*sort hypotheses*)
   hyps: term OrdList.T,                         (*hypotheses*)
   tpairs: (term * term) list,                   (*flex-flex pairs*)
   prop: term}                                   (*conclusion*)
 and deriv = Deriv of
  {promises: (serial * thm future) OrdList.T,
-  body: Pt.proof_body};
+  body: Pt.proof_body}
+with
 
 type conv = cterm -> thm;
 
 (*attributes subsume any kind of rules or context modifiers*)
 type attribute = Context.generic * thm -> Context.generic * thm;

           tpairs = [],
           prop = prop})
       end
   end;
 
+end;
+end;
+end;
+
 
 (* authentic derivation names *)
 
 fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);