# HG changeset patch
# User narasche
# Date 882534621 -3600
# Node ID ad8be126603d484a0243c9d2c719a1f00201bec9
# Parent  6e6d99e06d0c24fafbcdeafef7ce6f419e220cea
remove signatrue from records

diff -r 6e6d99e06d0c -r ad8be126603d src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Fri Dec 19 12:16:32 1997 +0100
+++ b/src/HOL/thy_data.ML	Fri Dec 19 13:30:21 1997 +0100
@@ -7,10 +7,9 @@
 
 (*for records*)
 type record_info =
- {args:     string list,
+ {args:     (string * sort) list,
   parent:   (typ list * string) option,
-  fields:   (string * typ) list,
-  sign_ref: Sign.sg_ref};
+  fields:   (string * typ) list}
 
 (*for datatypes*)
 type datatype_info =
@@ -26,8 +25,8 @@
 
 signature THY_DATA =
 sig
-  val get_records: theory -> record_info Symtab.table;
-  val put_records: record_info Symtab.table -> theory -> theory;
+  val get_records: theory -> record_info Symtab.table
+  val put_records: record_info Symtab.table -> theory -> theory
   val get_datatypes_sg: Sign.sg -> datatype_info Symtab.table
   val get_datatypes: theory -> datatype_info Symtab.table
   val put_datatypes: datatype_info Symtab.table -> theory -> theory
@@ -96,22 +95,20 @@
 
   fun print sg (Records tab) =
     let
-      fun pretty_args args = Pretty.lst ("(", ")") (map Pretty.str args);
+      fun pretty_parent None = []
+        | pretty_parent (Some (ts, name)) = 
+            [Pretty.block ((Sign.pretty_typ sg (Type (name, ts))) :: [Pretty.str (" +")])];
 
-      fun pretty_parent sign None = []
-        | pretty_parent sign (Some (ts, name)) = 
-            (Pretty.lst ("(", ")") (map (Sign.pretty_typ sign) ts)) :: [Pretty.str (name ^ " +")];
+      fun pretty_field (c, T) = Pretty.block
+        [Pretty.str (c ^ " :: "), Pretty.brk 1, Pretty.quote (Sign.pretty_typ sg T)];
 
-      fun pretty_field sign (c, T) = Pretty.block
-        [Pretty.str (c ^ " :: "), Pretty.brk 1, Pretty.quote (Sign.pretty_typ sign T)];
-
-      fun pretty_record (name, {args, parent, fields, sign_ref}) =
-        let val sign = Sign.deref sign_ref in
-          Pretty.block 
-            (Pretty.fbreaks
-              ((Pretty.block ((pretty_args args) :: [Pretty.str (" " ^ name ^ " =")])) ::
-              pretty_parent sign parent @ map (pretty_field sign) fields))
-        end
+      fun pretty_record (name, {args, parent, fields}) =
+        Pretty.block 
+          (Pretty.fbreaks
+            ((Pretty.block 
+                ((Sign.pretty_typ sg (Type (name, map TFree args))) :: 
+                   [Pretty.str " = "])) 
+              :: pretty_parent parent @ map pretty_field fields))
     in
       seq (Pretty.writeln o pretty_record) (Symtab.dest tab)
     end;