replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;

--- a/src/Pure/General/binding.ML	Wed Sep 16 13:43:15 2009 +0200
+++ b/src/Pure/General/binding.ML	Wed Sep 16 21:14:08 2009 +0200
@@ -30,18 +30,19 @@
   val str_of: binding -> string
 end;
 
-structure Binding:> BINDING =
+structure Binding: BINDING =
 struct
 
 (** representation **)
 
 (* datatype *)
 
-datatype binding = Binding of
+abstype binding = Binding of
  {prefix: (string * bool) list,     (*system prefix*)
   qualifier: (string * bool) list,  (*user qualifier*)
   name: bstring,                    (*base name*)
-  pos: Position.T};                 (*source position*)
+  pos: Position.T}                  (*source position*)
+with
 
 fun make_binding (prefix, qualifier, name, pos) =
   Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
@@ -109,6 +110,7 @@
   in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
 
 end;
+end;
 
 type binding = Binding.binding;
 

--- a/src/Pure/thm.ML	Wed Sep 16 13:43:15 2009 +0200
+++ b/src/Pure/thm.ML	Wed Sep 16 21:14:08 2009 +0200
@@ -153,7 +153,7 @@
   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
 
-structure Thm:> THM =
+structure Thm: THM =
 struct
 
 structure Pt = Proofterm;
@@ -163,11 +163,12 @@
 
 (** 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;
@@ -189,12 +190,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 OrdList.T};
+  sorts: sort OrdList.T}
+with
 
 exception CTERM of string * cterm list;
 
@@ -337,7 +339,7 @@
 
 (*** 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*)
@@ -348,7 +350,8 @@
   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;
 
@@ -1718,6 +1721,10 @@
       end
   end;
 
+end;
+end;
+end;
+
 
 (* authentic derivation names *)