accomodate tuned version of theory data;

--- a/src/HOL/Tools/record_package.ML	Fri Jun 05 14:32:23 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Fri Jun 05 14:33:18 1998 +0200
@@ -256,14 +256,13 @@
   simps: tthm list};
 
 
-(* theory data *)
-
-val recordsK = "HOL/records";
-exception Records of record_info Symtab.table;
-
-fun print_records thy = Display.print_data thy recordsK;
+(* data kind 'records' *)
 
 local
+  val recordsK = Object.kind "HOL/records";
+  exception Records of record_info Symtab.table;
+
+
   val empty = Records Symtab.empty;
 
   fun prep_ext (x as Records _) = x;
@@ -290,22 +289,17 @@
       seq (Pretty.writeln o pretty_record) (Symtab.dest tab)
     end;
 in
-  val record_thy_data = (recordsK, (empty, prep_ext, merge, print));
+  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;
 
 
 (* get and put records *)
 
-fun get_records thy =
-  (case Theory.get_data thy recordsK of
-    Records tab => tab
-  | _ => type_error recordsK);
-
 fun get_record thy name = Symtab.lookup (get_records thy, name);
 
-fun put_records tab thy =
-  Theory.put_data (recordsK, Records tab) thy;
-
 fun put_record name info thy =
   put_records (Symtab.update ((name, info), get_records thy)) thy;
 
@@ -707,7 +701,7 @@
 (** setup theory **)
 
 val setup =
- [Theory.init_data [record_thy_data],
+ [init_records,
   Theory.add_trfuns
     ([], [("_record", record_tr), ("_record_scheme", record_scheme_tr)], [], [])];
 

--- a/src/HOL/thy_data.ML	Fri Jun 05 14:32:23 1998 +0200
+++ b/src/HOL/thy_data.ML	Fri Jun 05 14:33:18 1998 +0200
@@ -5,7 +5,6 @@
 HOL theory data: datatypes.
 *)
 
-(*for datatypes*)
 type datatype_info =
  {case_const: term,
   case_rewrites: thm list,
@@ -29,14 +28,12 @@
 struct
 
 
-(** datatypes **)
-
 (* data kind 'datatypes' *)
 
-val datatypesK = "HOL/datatypes";
-exception DatatypeInfo of datatype_info Symtab.table;
+local
+  val datatypesK = Object.kind "HOL/datatypes";
+  exception DatatypeInfo of datatype_info Symtab.table;
 
-local
   val empty = DatatypeInfo Symtab.empty;
 
   fun prep_ext (x as DatatypeInfo _) = x;
@@ -48,27 +45,16 @@
     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));
+  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;
 
 
-(* get and put datatypes *)
-
-fun get_datatypes_sg sg =
-  (case Sign.get_data sg datatypesK of
-    DatatypeInfo tab => tab
-  | _ => type_error datatypesK);
-
-val get_datatypes = get_datatypes_sg o sign_of;
+(* setup *)
 
-fun put_datatypes tab thy =
-  Theory.put_data (datatypesK, DatatypeInfo tab) thy;
-
-
-
-(** theory data setup **)
-
-val setup = [Theory.init_data [datatypes_thy_data]];
+val setup = [init_datatypes];
 
 
 end;

--- a/src/Provers/classical.ML	Fri Jun 05 14:32:23 1998 +0200
+++ b/src/Provers/classical.ML	Fri Jun 05 14:33:18 1998 +0200
@@ -26,11 +26,12 @@
 
 signature CLASET_THY_DATA =
 sig
-  val clasetK: string
-  exception ClasetData of object ref
+  val clasetN: string
+  val clasetK: Object.kind
+  exception ClasetData of Object.T ref
   val setup: (theory -> theory) list
-  val fix_methods: object * (object -> object) *
-    (object * object -> object) * (Sign.sg -> object -> unit) -> unit
+  val fix_methods: Object.T * (Object.T -> Object.T) *
+    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit) -> unit
 end;
 
 signature CLASSICAL_DATA =
@@ -139,23 +140,24 @@
 
 (* data kind claset -- forward declaration *)
 
-val clasetK = "Provers/claset";
-exception ClasetData of object ref;
+val clasetN = "Provers/claset";
+val clasetK = Object.kind clasetN;
+exception ClasetData of Object.T ref;
 
 local
   fun undef _ = raise Match;
 
   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: Sign.sg -> object -> unit);
+  val prep_ext_fn = ref (undef: Object.T -> Object.T);
+  val merge_fn = ref (undef: Object.T * Object.T -> Object.T);
+  val print_fn = ref (undef: Sign.sg -> Object.T -> unit);
 
   val empty = ClasetData empty_ref;
   fun prep_ext exn = ! prep_ext_fn exn;
   fun merge exn = ! merge_fn exn;
   fun print sg exn = ! print_fn sg exn;
 in
-  val setup = [Theory.init_data [(clasetK, (empty, prep_ext, merge, print))]];
+  val setup = [Theory.init_data clasetK (empty, prep_ext, merge, print)];
   fun fix_methods (e, ext, mrg, prt) =
     (empty_ref := e; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt);
 end;
@@ -754,12 +756,9 @@
 
 (* access claset *)
 
-fun print_claset thy = Display.print_data thy clasetK;
+val print_claset = Theory.print_data clasetK;
 
-fun claset_ref_of_sg sg =
-  (case Sign.get_data sg clasetK of
-    ClasetData (ref (CSData r)) => r
-  | _ => type_error clasetK);
+val claset_ref_of_sg = Sign.get_data clasetK (fn ClasetData (ref (CSData r)) => r);
 
 val claset_ref_of = claset_ref_of_sg o sign_of;
 val claset_of_sg = ! o claset_ref_of_sg;

--- a/src/Provers/simplifier.ML	Fri Jun 05 14:32:23 1998 +0200
+++ b/src/Provers/simplifier.ML	Fri Jun 05 14:33:18 1998 +0200
@@ -254,7 +254,8 @@
 
 (** simpset data **)
 
-val simpsetK = "Provers/simpset";
+val simpsetN = "Provers/simpset";
+val simpsetK = Object.kind simpsetN;
 
 
 (* global simpset ref *)
@@ -272,18 +273,15 @@
 
   fun print _ (SimpsetGlobal (ref ss)) = print_ss ss;
 in
-  val setup_thy_data = Theory.init_data [(simpsetK, (empty, prep_ext, merge, print))];
+  val setup_thy_data = Theory.init_data simpsetK (empty, prep_ext, merge, print);
 end;
 
 
 (* access global simpset *)
 
-fun print_simpset thy = Display.print_data thy simpsetK;
+val print_simpset = Theory.print_data simpsetK;
 
-fun simpset_ref_of_sg sg =
-  (case Sign.get_data sg simpsetK of
-    SimpsetGlobal r => r
-  | _ => type_error simpsetK);
+val simpset_ref_of_sg = Sign.get_data simpsetK (fn SimpsetGlobal r => r);
 
 val simpset_ref_of = simpset_ref_of_sg o sign_of;
 val simpset_of_sg = ! o simpset_ref_of_sg;
@@ -311,13 +309,13 @@
 exception SimpsetLocal of simpset;
 
 fun get_local_simpset (thy, data) =
-  (case Symtab.lookup (data, simpsetK) of
+  (case Symtab.lookup (data, simpsetN) of
     Some (SimpsetLocal ss) => ss
   | None => simpset_of thy
-  | _ => type_error simpsetK);
+  | _ => Object.kind_error simpsetK);
 
 fun put_local_simpset ss (thy, data) =
-  (thy, Symtab.update ((simpsetK, SimpsetLocal ss), data));
+  (thy, Symtab.update ((simpsetN, SimpsetLocal ss), data));
 
 
 
@@ -353,7 +351,8 @@
   val simp_attr_global = simp_attr change_global_ss;
   val simp_attr_local = simp_attr change_local_ss;
 in
-  val setup_attrs = Attribute.add_attrs [(simpN, (simp_attr_global, simp_attr_local))];
+  val setup_attrs = Attribute.add_attributes
+    [(simpN, simp_attr_global, simp_attr_local, "simplifier")];
 
   val simp_add_global = simp_attr_global [simp_addN];
   val simp_del_global = simp_attr_global [simp_delN];