replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
authorwenzelm
Wed Sep 16 21:14:08 2009 +0200 (2009-09-16)
changeset 3259095f4f08f950f
parent 32589 9353798ce61f
child 32591 9433e7435b9b
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
src/Pure/General/binding.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/General/binding.ML	Wed Sep 16 13:43:15 2009 +0200
     1.2 +++ b/src/Pure/General/binding.ML	Wed Sep 16 21:14:08 2009 +0200
     1.3 @@ -30,18 +30,19 @@
     1.4    val str_of: binding -> string
     1.5  end;
     1.6  
     1.7 -structure Binding:> BINDING =
     1.8 +structure Binding: BINDING =
     1.9  struct
    1.10  
    1.11  (** representation **)
    1.12  
    1.13  (* datatype *)
    1.14  
    1.15 -datatype binding = Binding of
    1.16 +abstype binding = Binding of
    1.17   {prefix: (string * bool) list,     (*system prefix*)
    1.18    qualifier: (string * bool) list,  (*user qualifier*)
    1.19    name: bstring,                    (*base name*)
    1.20 -  pos: Position.T};                 (*source position*)
    1.21 +  pos: Position.T}                  (*source position*)
    1.22 +with
    1.23  
    1.24  fun make_binding (prefix, qualifier, name, pos) =
    1.25    Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
    1.26 @@ -109,6 +110,7 @@
    1.27    in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
    1.28  
    1.29  end;
    1.30 +end;
    1.31  
    1.32  type binding = Binding.binding;
    1.33  
     2.1 --- a/src/Pure/thm.ML	Wed Sep 16 13:43:15 2009 +0200
     2.2 +++ b/src/Pure/thm.ML	Wed Sep 16 21:14:08 2009 +0200
     2.3 @@ -153,7 +153,7 @@
     2.4    val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
     2.5  end;
     2.6  
     2.7 -structure Thm:> THM =
     2.8 +structure Thm: THM =
     2.9  struct
    2.10  
    2.11  structure Pt = Proofterm;
    2.12 @@ -163,11 +163,12 @@
    2.13  
    2.14  (** certified types **)
    2.15  
    2.16 -datatype ctyp = Ctyp of
    2.17 +abstype ctyp = Ctyp of
    2.18   {thy_ref: theory_ref,
    2.19    T: typ,
    2.20    maxidx: int,
    2.21 -  sorts: sort OrdList.T};
    2.22 +  sorts: sort OrdList.T}
    2.23 +with
    2.24  
    2.25  fun rep_ctyp (Ctyp args) = args;
    2.26  fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
    2.27 @@ -189,12 +190,13 @@
    2.28  (** certified terms **)
    2.29  
    2.30  (*certified terms with checked typ, maxidx, and sorts*)
    2.31 -datatype cterm = Cterm of
    2.32 +abstype cterm = Cterm of
    2.33   {thy_ref: theory_ref,
    2.34    t: term,
    2.35    T: typ,
    2.36    maxidx: int,
    2.37 -  sorts: sort OrdList.T};
    2.38 +  sorts: sort OrdList.T}
    2.39 +with
    2.40  
    2.41  exception CTERM of string * cterm list;
    2.42  
    2.43 @@ -337,7 +339,7 @@
    2.44  
    2.45  (*** Derivations and Theorems ***)
    2.46  
    2.47 -datatype thm = Thm of
    2.48 +abstype thm = Thm of
    2.49   deriv *                                        (*derivation*)
    2.50   {thy_ref: theory_ref,                          (*dynamic reference to theory*)
    2.51    tags: Properties.T,                           (*additional annotations/comments*)
    2.52 @@ -348,7 +350,8 @@
    2.53    prop: term}                                   (*conclusion*)
    2.54  and deriv = Deriv of
    2.55   {promises: (serial * thm future) OrdList.T,
    2.56 -  body: Pt.proof_body};
    2.57 +  body: Pt.proof_body}
    2.58 +with
    2.59  
    2.60  type conv = cterm -> thm;
    2.61  
    2.62 @@ -1718,6 +1721,10 @@
    2.63        end
    2.64    end;
    2.65  
    2.66 +end;
    2.67 +end;
    2.68 +end;
    2.69 +
    2.70  
    2.71  (* authentic derivation names *)
    2.72