adapted print methods;

--- a/src/HOL/thy_data.ML	Thu Nov 20 15:30:37 1997 +0100
+++ b/src/HOL/thy_data.ML	Thu Nov 20 15:36:09 1997 +0100
@@ -8,7 +8,7 @@
 (*for records*)
 type record_info =
  {parent: string option,
-  fields: (string * ctyp) list};
+  fields: (string * typ) list};
 
 (*for datatypes*)
 type datatype_info =
@@ -30,7 +30,7 @@
   val get_datatypes: theory -> datatype_info Symtab.table
   val put_datatypes: datatype_info Symtab.table -> theory -> theory
   val hol_data: (string * (object * (object -> object) *
-    (object * object -> object) * (object -> unit))) list
+    (object * object -> object) * (Sign.sg -> object -> unit))) list
 end;
 
 structure ThyData: THY_DATA =
@@ -52,8 +52,9 @@
   fun merge (DatatypeInfo tab1, DatatypeInfo tab2) =
     DatatypeInfo (Symtab.merge (K true) (tab1, tab2));
 
-  fun print (DatatypeInfo tab) =
-    Pretty.writeln (Pretty.strs ("datatypes:" :: map fst (Symtab.dest tab)));
+  fun print sg (DatatypeInfo tab) =
+    Pretty.writeln (Pretty.strs ("datatypes:" ::
+      map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
 in
   val datatypes_thy_data = (datatypesK, (empty, prep_ext, merge, print));
 end;
@@ -91,13 +92,15 @@
   fun merge (Records tab1, Records tab2) =
     Records (Symtab.merge (K true) (tab1, tab2));
 
-  fun print (Records tab) =
+  fun print sg (Records tab) =
     let
       fun pretty_parent None = []
-        | pretty_parent (Some name) = [Pretty.str (name ^ " +")];
+        | pretty_parent (Some name) =
+            [Pretty.str (Sign.cond_extern sg Sign.typeK name ^ " +")];
 
       fun pretty_field (c, T) = Pretty.block
-        [Pretty.str (c ^ " :: "), Pretty.brk 1, Pretty.quote (Display.pretty_ctyp T)];
+        [Pretty.str (Sign.cond_extern sg Sign.constK c ^ " :: "),
+          Pretty.brk 1, Pretty.quote (Sign.pretty_typ sg T)];
 
       fun pretty_record (name, {parent, fields}) =
         Pretty.big_list (name ^ " =") (pretty_parent parent @ map pretty_field fields);
@@ -124,8 +127,8 @@
 (** hol_data **)
 
 val hol_data =
- [Simplifier.simpset_thy_data,          (*see Provers/simplifier.ML*)
-  ClasetThyData.thy_data,               (*see Provers/classical.ML*)
+ [Simplifier.simpset_thy_data,
+  ClasetThyData.thy_data,
   datatypes_thy_data,
   record_thy_data];
 

--- a/src/Provers/classical.ML	Thu Nov 20 15:30:37 1997 +0100
+++ b/src/Provers/classical.ML	Thu Nov 20 15:36:09 1997 +0100
@@ -28,9 +28,9 @@
   val clasetK: string
   exception ClasetData of object ref
   val thy_data: string * (object * (object -> object) *
-    (object * object -> object) * (object -> unit))
+    (object * object -> object) * (Sign.sg -> object -> unit))
   val fix_methods: object * (object -> object) *
-    (object * object -> object) * (object -> unit) -> unit
+    (object * object -> object) * (Sign.sg -> object -> unit) -> unit
 end;
 
 signature CLASSICAL_DATA =
@@ -147,12 +147,12 @@
   val empty_ref = ref ERROR;
   val prep_ext_fn = ref (undef: object -> object);
   val merge_fn = ref (undef: object * object -> object);
-  val print_fn = ref (undef: object -> unit);
+  val print_fn = ref (undef: Sign.sg -> object -> unit);
 
   val empty = ClasetData empty_ref;
   fun prep_ext exn = ! prep_ext_fn exn;
   fun merge exn = ! merge_fn exn;
-  fun print exn = ! print_fn exn;
+  fun print sg exn = ! print_fn sg exn;
 in
   val thy_data = (clasetK, (empty, prep_ext, merge, print));
   fun fix_methods (e, ext, mrg, prt) =
@@ -728,7 +728,7 @@
   fun merge (ClasetData (ref (CSData (ref cs1))), ClasetData (ref (CSData (ref cs2)))) =
     ClasetData (ref (CSData (ref (merge_cs (cs1, cs2)))));
 
-  fun print (ClasetData (ref (CSData (ref cs)))) = print_cs cs;
+  fun print (_: Sign.sg) (ClasetData (ref (CSData (ref cs)))) = print_cs cs;
 in
   val _ = fix_methods (empty, prep_ext, merge, print);
 end;

--- a/src/Provers/simplifier.ML	Thu Nov 20 15:30:37 1997 +0100
+++ b/src/Provers/simplifier.ML	Thu Nov 20 15:36:09 1997 +0100
@@ -47,7 +47,7 @@
   val prems_of_ss:  simpset -> thm list
 
   val simpset_thy_data: string * (object * (object -> object) *
-    (object * object -> object) * (object -> unit))
+    (object * object -> object) * (Sign.sg -> object -> unit))
   val simpset_ref_of_sg: Sign.sg -> simpset ref
   val simpset_ref_of: theory -> simpset ref
   val simpset_of_sg: Sign.sg -> simpset
@@ -259,7 +259,7 @@
   fun merge (SimpsetData (ref ss1), SimpsetData (ref ss2)) =
     SimpsetData (ref (merge_ss (ss1, ss2)));
 
-  fun print (SimpsetData (ref ss)) = print_ss ss;
+  fun print (_: Sign.sg) (SimpsetData (ref ss)) = print_ss ss;
 in
   val simpset_thy_data = (simpsetK, (empty, prep_ext, merge, print));
 end;