--- 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];