# HG changeset patch
# User wenzelm
# Date 893843202 -7200
# Node ID 1c502a82bcde4bdc9d4bdbc051f5d122d0175f47
# Parent  cb48549230cecdab16334cee9d1f3bfb1dc7e1f8
moved records data to Tools/record_package.ML;
tuned setup;

diff -r cb48549230ce -r 1c502a82bcde src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Wed Apr 29 11:45:41 1998 +0200
+++ b/src/HOL/thy_data.ML	Wed Apr 29 11:46:42 1998 +0200
@@ -2,15 +2,9 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-HOL theory data: records, datatypes.
+HOL theory data: datatypes.
 *)
 
-(*for records*)
-type record_info =
- {args: (string * sort) list,
-  parent: (typ list * string) option,
-  fields: (string * typ) list}
-
 (*for datatypes*)
 type datatype_info =
  {case_const: term,
@@ -25,12 +19,10 @@
 
 signature THY_DATA =
 sig
-  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
-  val setup: theory -> theory
+  val setup: (theory -> theory) list
 end;
 
 structure ThyData: THY_DATA =
@@ -74,63 +66,9 @@
 
 
 
-(** records **)
-
-(* data kind 'records' *)
-
-val recordsK = "HOL/records";
-exception Records of record_info Symtab.table;
-
-
-(* methods *)
-
-local
-  val empty = Records Symtab.empty;
-
-  fun prep_ext (x as Records _) = x;
-
-  fun merge (Records tab1, Records tab2) =
-    Records (Symtab.merge (K true) (tab1, tab2));
-
-  fun print sg (Records tab) =
-    let
-      fun pretty_parent None = []
-        | pretty_parent (Some (ts, name)) = 
-            [Pretty.block ((Sign.pretty_typ sg (Type (name, ts))) :: [Pretty.str (" +")])];
-
-      fun pretty_field (c, T) = Pretty.block
-        [Pretty.str (c ^ " :: "), Pretty.brk 1, Pretty.quote (Sign.pretty_typ sg T)];
-
-      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;
-in
-  val record_thy_data = (recordsK, (empty, prep_ext, merge, print));
-end;
-
-
-(* get and put records *)
-
-fun get_records thy =
-  (case Theory.get_data thy recordsK of
-    Records tab => tab
-  | _ => type_error recordsK);
-
-fun put_records tab thy =
-  Theory.put_data (recordsK, Records tab) thy;
-
-
-
 (** theory data setup **)
 
-val setup = Theory.init_data [datatypes_thy_data, record_thy_data];
+val setup = [Theory.init_data [datatypes_thy_data]];
 
 
 end;