# HG changeset patch
# User wenzelm
# Date 897385072 -7200
# Node ID cdc86a914e633dfe5bc9bcf64dc3614fe5750c96
# Parent  4486d53a6438bab653e6d1ae93af8195a19b00d5
adapted to new theory data interface;

diff -r 4486d53a6438 -r cdc86a914e63 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon Jun 08 15:58:56 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Jun 09 11:37:52 1998 +0200
@@ -256,21 +256,18 @@
   simps: tthm list};
 
 
-(* data kind 'records' *)
-
-local
-  val recordsK = Object.kind "HOL/records";
-  exception Records of record_info Symtab.table;
-
+(* data kind '"HOL/records' *)
 
-  val empty = Records Symtab.empty;
-
-  fun prep_ext (x as Records _) = x;
+structure RecordsArgs =
+struct
+  val name = "HOL/records";
+  type T = record_info Symtab.table;
 
-  fun merge (Records tab1, Records tab2) =
-    Records (Symtab.merge (K true) (tab1, tab2));
+  val empty = Symtab.empty;
+  val prep_ext = I;
+  val merge: T * T -> T = Symtab.merge (K true);
 
-  fun print sg (Records tab) =
+  fun print sg tab =
     let
       val prt_typ = Sign.pretty_typ sg;
       val ext_const = Sign.cond_extern sg Sign.constK;
@@ -288,20 +285,18 @@
     in
       seq (Pretty.writeln o pretty_record) (Symtab.dest tab)
     end;
-in
-  val init_records = Theory.init_data recordsK (empty, prep_ext, merge, print);
-  val print_records = Theory.print_data recordsK;
-  val get_records = Theory.get_data recordsK (fn Records x => x);
-  val put_records = Theory.put_data recordsK Records;
 end;
 
+structure RecordsData = TheoryDataFun(RecordsArgs);
+val print_records = RecordsData.print;
+
 
 (* get and put records *)
 
-fun get_record thy name = Symtab.lookup (get_records thy, name);
+fun get_record thy name = Symtab.lookup (RecordsData.get thy, name);
 
 fun put_record name info thy =
-  put_records (Symtab.update ((name, info), get_records thy)) thy;
+  RecordsData.put (Symtab.update ((name, info), RecordsData.get thy)) thy;
 
 
 (* parent records *)
@@ -701,7 +696,7 @@
 (** setup theory **)
 
 val setup =
- [init_records,
+ [RecordsData.init,
   Theory.add_trfuns
     ([], [("_record", record_tr), ("_record_scheme", record_scheme_tr)], [], [])];
 
diff -r 4486d53a6438 -r cdc86a914e63 src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Mon Jun 08 15:58:56 1998 +0200
+++ b/src/HOL/thy_data.ML	Tue Jun 09 11:37:52 1998 +0200
@@ -28,33 +28,31 @@
 struct
 
 
-(* data kind 'datatypes' *)
-
-local
-  val datatypesK = Object.kind "HOL/datatypes";
-  exception DatatypeInfo of datatype_info Symtab.table;
+(* data kind 'HOL/datatypes' *)
 
-  val empty = DatatypeInfo Symtab.empty;
-
-  fun prep_ext (x as DatatypeInfo _) = x;
+structure DatatypesArgs =
+struct
+  val name = "HOL/datatypes";
+  type T = datatype_info Symtab.table;
 
-  fun merge (DatatypeInfo tab1, DatatypeInfo tab2) =
-    DatatypeInfo (Symtab.merge (K true) (tab1, tab2));
+  val empty = Symtab.empty;
+  val prep_ext = I;
+  val merge: T * T -> T = Symtab.merge (K true);
 
-  fun print sg (DatatypeInfo tab) =
+  fun print sg tab =
     Pretty.writeln (Pretty.strs ("datatypes:" ::
       map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
-in
-  val init_datatypes = Theory.init_data datatypesK (empty, prep_ext, merge, print);
-  val get_datatypes_sg = Sign.get_data datatypesK (fn DatatypeInfo tab => tab);
-  val get_datatypes = get_datatypes_sg o sign_of;
-  val put_datatypes = Theory.put_data datatypesK DatatypeInfo;
 end;
 
+structure DatatypesData = TheoryDataFun(DatatypesArgs);
+val get_datatypes_sg = DatatypesData.get_sg;
+val get_datatypes = DatatypesData.get;
+val put_datatypes = DatatypesData.put;
+
 
 (* setup *)
 
-val setup = [init_datatypes];
+val setup = [DatatypesData.init];
 
 
 end;