old-fashioned abstype ctyp/cterm/thm prevents accidental equality tests;

--- a/src/Pure/thm.ML	Sun Feb 04 22:02:16 2007 +0100
+++ b/src/Pure/thm.ML	Sun Feb 04 22:02:17 2007 +0100
@@ -181,6 +181,8 @@
 structure Thm: THM =
 struct
 
+structure Pt = Proofterm;
+
 
 (*** Certified terms and types ***)
 
@@ -198,11 +200,12 @@
 
 (** certified types **)
 
-datatype ctyp = Ctyp of
+abstype ctyp = Ctyp of
  {thy_ref: theory_ref,
   T: typ,
   maxidx: int,
-  sorts: sort list};
+  sorts: sort list}
+with
 
 fun rep_ctyp (Ctyp {thy_ref, T, maxidx, sorts}) =
   let val thy = Theory.deref thy_ref
@@ -233,12 +236,13 @@
 (** 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 list};
+  sorts: sort list}
+with
 
 exception CTERM of string;
 
@@ -380,11 +384,9 @@
 
 (*** Meta theorems ***)
 
-structure Pt = Proofterm;
-
 type tag = string * string list;
 
-datatype thm = Thm of
+abstype thm = Thm of
  {thy_ref: theory_ref,         (*dynamic reference to theory*)
   der: bool * Pt.proof,        (*derivation*)
   tags: tag list,              (*additional annotations/comments*)
@@ -392,7 +394,8 @@
   shyps: sort list,            (*sort hypotheses as ordered list*)
   hyps: term list,             (*hypotheses as ordered list*)
   tpairs: (term * term) list,  (*flex-flex pairs*)
-  prop: term};                 (*conclusion*)
+  prop: term}                  (*conclusion*)
+with
 
 (*errors involving theorems*)
 exception THM of string * int * thm list;
@@ -1679,6 +1682,10 @@
 fun invoke_oracle thy =
   invoke_oracle_i thy o NameSpace.intern (Theory.oracle_space thy);
 
+
+end;
+end;
+end;
 end;
 
 structure BasicThm: BASIC_THM = Thm;