src/Pure/thm.ML
changeset 32590 95f4f08f950f
parent 32198 9bdd47909ea8
child 32725 57e29093ecfb
     1.1 --- a/src/Pure/thm.ML	Wed Sep 16 13:43:15 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Wed Sep 16 21:14:08 2009 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4    val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
     1.5  end;
     1.6  
     1.7 -structure Thm:> THM =
     1.8 +structure Thm: THM =
     1.9  struct
    1.10  
    1.11  structure Pt = Proofterm;
    1.12 @@ -163,11 +163,12 @@
    1.13  
    1.14  (** certified types **)
    1.15  
    1.16 -datatype ctyp = Ctyp of
    1.17 +abstype ctyp = Ctyp of
    1.18   {thy_ref: theory_ref,
    1.19    T: typ,
    1.20    maxidx: int,
    1.21 -  sorts: sort OrdList.T};
    1.22 +  sorts: sort OrdList.T}
    1.23 +with
    1.24  
    1.25  fun rep_ctyp (Ctyp args) = args;
    1.26  fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
    1.27 @@ -189,12 +190,13 @@
    1.28  (** certified terms **)
    1.29  
    1.30  (*certified terms with checked typ, maxidx, and sorts*)
    1.31 -datatype cterm = Cterm of
    1.32 +abstype cterm = Cterm of
    1.33   {thy_ref: theory_ref,
    1.34    t: term,
    1.35    T: typ,
    1.36    maxidx: int,
    1.37 -  sorts: sort OrdList.T};
    1.38 +  sorts: sort OrdList.T}
    1.39 +with
    1.40  
    1.41  exception CTERM of string * cterm list;
    1.42  
    1.43 @@ -337,7 +339,7 @@
    1.44  
    1.45  (*** Derivations and Theorems ***)
    1.46  
    1.47 -datatype thm = Thm of
    1.48 +abstype thm = Thm of
    1.49   deriv *                                        (*derivation*)
    1.50   {thy_ref: theory_ref,                          (*dynamic reference to theory*)
    1.51    tags: Properties.T,                           (*additional annotations/comments*)
    1.52 @@ -348,7 +350,8 @@
    1.53    prop: term}                                   (*conclusion*)
    1.54  and deriv = Deriv of
    1.55   {promises: (serial * thm future) OrdList.T,
    1.56 -  body: Pt.proof_body};
    1.57 +  body: Pt.proof_body}
    1.58 +with
    1.59  
    1.60  type conv = cterm -> thm;
    1.61  
    1.62 @@ -1718,6 +1721,10 @@
    1.63        end
    1.64    end;
    1.65  
    1.66 +end;
    1.67 +end;
    1.68 +end;
    1.69 +
    1.70  
    1.71  (* authentic derivation names *)
    1.72