--- a/src/HOL/Boogie/Tools/boogie_split.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_split.ML Sun Nov 08 18:43:42 2009 +0100
@@ -18,13 +18,12 @@
(* sub-tactics store *)
-structure Sub_Tactics = TheoryDataFun
+structure Sub_Tactics = Theory_Data
(
type T = (Proof.context -> int -> tactic) Symtab.table
val empty = Symtab.empty
- val copy = I
val extend = I
- fun merge _ = Symtab.merge (K true)
+ fun merge data = Symtab.merge (K true) data
)
fun add_sub_tactic tac = Sub_Tactics.map (Symtab.update_new tac)
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Sun Nov 08 18:43:42 2009 +0100
@@ -19,14 +19,13 @@
fun err_vcs () = error "undischarged Boogie verification conditions found"
-structure VCs = TheoryDataFun
+structure VCs = Theory_Data
(
- type T = (Term.term * bool) Symtab.table option
+ type T = (term * bool) Symtab.table option
val empty = NONE
- val copy = I
val extend = I
- fun merge _ (NONE, NONE) = NONE
- | merge _ (_, _) = err_vcs ()
+ fun merge (NONE, NONE) = NONE
+ | merge _ = err_vcs ()
)
fun set vcs = VCs.map (fn
--- a/src/HOL/Import/hol4rews.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Import/hol4rews.ML Sun Nov 08 18:43:42 2009 +0100
@@ -11,25 +11,23 @@
| Generating of string
| Replaying of string
-structure HOL4DefThy = TheoryDataFun
+structure HOL4DefThy = Theory_Data
(
type T = ImportStatus
val empty = NoImport
- val copy = I
val extend = I
- fun merge _ (NoImport,NoImport) = NoImport
- | merge _ _ = (warning "Import status set during merge"; NoImport)
+ fun merge (NoImport, NoImport) = NoImport
+ | merge _ = (warning "Import status set during merge"; NoImport)
)
-structure ImportSegment = TheoryDataFun
+structure ImportSegment = Theory_Data
(
type T = string
val empty = ""
- val copy = I
val extend = I
- fun merge _ ("",arg) = arg
- | merge _ (arg,"") = arg
- | merge _ (s1,s2) =
+ fun merge ("",arg) = arg
+ | merge (arg,"") = arg
+ | merge (s1,s2) =
if s1 = s2
then s1
else error "Trying to merge two different import segments"
@@ -38,42 +36,38 @@
val get_import_segment = ImportSegment.get
val set_import_segment = ImportSegment.put
-structure HOL4UNames = TheoryDataFun
+structure HOL4UNames = Theory_Data
(
type T = string list
val empty = []
- val copy = I
val extend = I
- fun merge _ ([],[]) = []
- | merge _ _ = error "Used names not empty during merge"
+ fun merge ([], []) = []
+ | merge _ = error "Used names not empty during merge"
)
-structure HOL4Dump = TheoryDataFun
+structure HOL4Dump = Theory_Data
(
type T = string * string * string list
val empty = ("","",[])
- val copy = I
val extend = I
- fun merge _ (("","",[]),("","",[])) = ("","",[])
- | merge _ _ = error "Dump data not empty during merge"
+ fun merge (("","",[]),("","",[])) = ("","",[])
+ | merge _ = error "Dump data not empty during merge"
)
-structure HOL4Moves = TheoryDataFun
+structure HOL4Moves = Theory_Data
(
type T = string Symtab.table
val empty = Symtab.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = Symtab.merge (K true)
+ fun merge data = Symtab.merge (K true) data
)
-structure HOL4Imports = TheoryDataFun
+structure HOL4Imports = Theory_Data
(
type T = string Symtab.table
val empty = Symtab.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = Symtab.merge (K true)
+ fun merge data = Symtab.merge (K true) data
)
fun get_segment2 thyname thy =
@@ -87,85 +81,76 @@
HOL4Imports.put imps' thy
end
-structure HOL4CMoves = TheoryDataFun
+structure HOL4CMoves = Theory_Data
(
type T = string Symtab.table
val empty = Symtab.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = Symtab.merge (K true)
+ fun merge data = Symtab.merge (K true) data
)
-structure HOL4Maps = TheoryDataFun
+structure HOL4Maps = Theory_Data
(
- type T = (string option) StringPair.table
+ type T = string option StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4Thms = TheoryDataFun
+structure HOL4Thms = Theory_Data
(
type T = holthm StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4ConstMaps = TheoryDataFun
+structure HOL4ConstMaps = Theory_Data
(
type T = (bool * string * typ option) StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4Rename = TheoryDataFun
+structure HOL4Rename = Theory_Data
(
type T = string StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4DefMaps = TheoryDataFun
+structure HOL4DefMaps = Theory_Data
(
type T = string StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4TypeMaps = TheoryDataFun
+structure HOL4TypeMaps = Theory_Data
(
type T = (bool * string) StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4Pending = TheoryDataFun
+structure HOL4Pending = Theory_Data
(
type T = ((term * term) list * thm) StringPair.table
val empty = StringPair.empty
- val copy = I
val extend = I
- fun merge _ : T * T -> T = StringPair.merge (K true)
+ fun merge data = StringPair.merge (K true) data
)
-structure HOL4Rewrites = TheoryDataFun
+structure HOL4Rewrites = Theory_Data
(
type T = thm list
val empty = []
- val copy = I
val extend = I
- fun merge _ = Library.merge Thm.eq_thm_prop
+ val merge = Thm.merge_thms
)
val hol4_debug = Unsynchronized.ref false
--- a/src/HOL/Import/import.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Import/import.ML Sun Nov 08 18:43:42 2009 +0100
@@ -9,13 +9,12 @@
val setup : theory -> theory
end
-structure ImportData = TheoryDataFun
+structure ImportData = Theory_Data
(
- type T = ProofKernel.thm option array option
+ type T = ProofKernel.thm option array option (* FIXME mutable array !??!!! *)
val empty = NONE
- val copy = I
val extend = I
- fun merge _ _ = NONE
+ fun merge _ = NONE
)
structure Import :> IMPORT =
--- a/src/HOL/Import/shuffler.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Import/shuffler.ML Sun Nov 08 18:43:42 2009 +0100
@@ -72,13 +72,12 @@
| _ => raise THM("Not an equality",0,[th]))
handle _ => raise THM("Couldn't make object equality",0,[th]) (* FIXME avoid handle _ *)
-structure ShuffleData = TheoryDataFun
+structure ShuffleData = Theory_Data
(
type T = thm list
val empty = []
- val copy = I
val extend = I
- fun merge _ = Library.merge Thm.eq_thm_prop
+ val merge = Thm.merge_thms
)
fun print_shuffles thy =
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Nov 08 18:43:42 2009 +0100
@@ -60,13 +60,12 @@
type run_action = int -> run_args -> unit
type action = init_action * run_action * done_action
-structure Actions = TheoryDataFun
+structure Actions = Theory_Data
(
type T = (int * run_action * done_action) list
val empty = []
- val copy = I
val extend = I
- fun merge _ = Library.merge (K true)
+ fun merge data = Library.merge (K true) data (* FIXME ?!? *)
)
--- a/src/HOL/Nominal/nominal_atoms.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Sun Nov 08 18:43:42 2009 +0100
@@ -42,13 +42,12 @@
cp_inst : thm Symtab.table,
dj_thms : thm Symtab.table};
-structure NominalData = TheoryDataFun
+structure NominalData = Theory_Data
(
type T = atom_info Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ x = Symtab.merge (K true) x;
+ fun merge data = Symtab.merge (K true) data;
);
fun make_atom_info ((((((pt_class, fs_class), cp_classes), at_inst), pt_inst), cp_inst), dj_thms) =
--- a/src/HOL/Nominal/nominal_datatype.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Nov 08 18:43:42 2009 +0100
@@ -84,13 +84,12 @@
distinct : thm list,
inject : thm list};
-structure NominalDatatypesData = TheoryDataFun
+structure NominalDatatypesData = Theory_Data
(
type T = nominal_datatype_info Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (K true) tabs;
+ fun merge data = Symtab.merge (K true) data;
);
val get_nominal_datatypes = NominalDatatypesData.get;
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Nov 08 18:43:42 2009 +0100
@@ -226,13 +226,12 @@
fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
-structure Provers = TheoryDataFun
+structure Provers = Theory_Data
(
type T = (ATP_Wrapper.prover * stamp) Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
+ fun merge data : T = Symtab.merge (eq_snd op =) data
handle Symtab.DUP dup => err_dup_prover dup;
);
--- a/src/HOL/Tools/Datatype/datatype.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sun Nov 08 18:43:42 2009 +0100
@@ -42,7 +42,7 @@
(* data management *)
-structure DatatypesData = TheoryDataFun
+structure DatatypesData = Theory_Data
(
type T =
{types: info Symtab.table,
@@ -51,11 +51,10 @@
val empty =
{types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
({types = types1, constrs = constrs1, cases = cases1},
- {types = types2, constrs = constrs2, cases = cases2}) =
+ {types = types2, constrs = constrs2, cases = cases2}) : T =
{types = Symtab.merge (K true) (types1, types2),
constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
cases = Symtab.merge (K true) (cases1, cases2)};
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Nov 08 18:43:42 2009 +0100
@@ -63,13 +63,12 @@
reduction_pair : thm
}
-structure Multiset_Setup = TheoryDataFun
+structure Multiset_Setup = Theory_Data
(
type T = multiset_setup option
val empty = NONE
- val copy = I;
val extend = I;
- fun merge _ (v1, v2) = if is_some v2 then v2 else v1
+ fun merge (v1, v2) = if is_some v2 then v2 else v1 (* FIXME prefer v1 !?! *)
)
val multiset_setup = Multiset_Setup.put o SOME
--- a/src/HOL/Tools/Function/size.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML Sun Nov 08 18:43:42 2009 +0100
@@ -15,13 +15,12 @@
open DatatypeAux;
-structure SizeData = TheoryDataFun
+structure SizeData = Theory_Data
(
type T = (string * thm list) Symtab.table;
val empty = Symtab.empty;
- val copy = I
val extend = I
- fun merge _ = Symtab.merge (K true);
+ fun merge data = Symtab.merge (K true) data;
);
val lookup_size = SizeData.get #> Symtab.lookup;
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Nov 08 18:43:42 2009 +0100
@@ -179,14 +179,13 @@
unrolled_preds: unrolled list Unsynchronized.ref,
wf_cache: wf_cache Unsynchronized.ref}
-structure TheoryData = TheoryDataFun(
+structure TheoryData = Theory_Data(
type T = {frac_types: (string * (string * string) list) list,
codatatypes: (string * (string * styp list)) list}
val empty = {frac_types = [], codatatypes = []}
- val copy = I
val extend = I
- fun merge _ ({frac_types = fs1, codatatypes = cs1},
- {frac_types = fs2, codatatypes = cs2}) =
+ fun merge ({frac_types = fs1, codatatypes = cs1},
+ {frac_types = fs2, codatatypes = cs2}) : T =
{frac_types = AList.merge (op =) (op =) (fs1, fs2),
codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Nov 08 18:43:42 2009 +0100
@@ -125,13 +125,12 @@
| _ => value)
| NONE => (name, value)
-structure TheoryData = TheoryDataFun(
+structure TheoryData = Theory_Data(
type T = {params: raw_param list, registered_auto: bool}
val empty = {params = rev default_default_params, registered_auto = false}
- val copy = I
val extend = I
- fun merge _ ({params = ps1, registered_auto = a1},
- {params = ps2, registered_auto = a2}) =
+ fun merge ({params = ps1, registered_auto = a1},
+ {params = ps2, registered_auto = a2}) : T =
{params = AList.merge (op =) (op =) (ps1, ps2),
registered_auto = a1 orelse a2})
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Nov 08 18:43:42 2009 +0100
@@ -232,13 +232,12 @@
eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso
#nparams d1 = #nparams d2
-structure PredData = TheoryDataFun
+structure PredData = Theory_Data
(
type T = pred_data Graph.T;
val empty = Graph.empty;
- val copy = I;
val extend = I;
- fun merge _ = Graph.merge eq_pred_data;
+ val merge = Graph.merge eq_pred_data;
);
(* queries *)
@@ -2450,7 +2449,7 @@
(*FIXME name discrepancy in attribs and ML code*)
(*FIXME intros should be better named intro*)
-(* TODO: make TheoryDataFun to Generic_Data & remove duplication of local theory and theory *)
+(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
fun generic_code_pred prep_const options raw_const lthy =
let
val thy = ProofContext.theory_of lthy
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Nov 08 18:43:42 2009 +0100
@@ -19,15 +19,14 @@
open Predicate_Compile_Aux;
-structure Data = TheoryDataFun
+structure Data = Theory_Data
(
type T =
{const_spec_table : thm list Symtab.table};
val empty =
{const_spec_table = Symtab.empty};
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
({const_spec_table = const_spec_table1},
{const_spec_table = const_spec_table2}) =
{const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sun Nov 08 18:43:42 2009 +0100
@@ -56,13 +56,12 @@
fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
(* Table from constant name (string) to term of inductive predicate *)
-structure Pred_Compile_Preproc = TheoryDataFun
+structure Pred_Compile_Preproc = Theory_Data
(
type T = string Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (op =);
+ fun merge data : T = Symtab.merge (op =) data; (* FIXME handle Symtab.DUP ?? *)
)
fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name
--- a/src/HOL/Tools/arith_data.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML Sun Nov 08 18:43:42 2009 +0100
@@ -41,13 +41,12 @@
val get_arith_facts = Arith_Facts.get;
-structure Arith_Tactics = TheoryDataFun
+structure Arith_Tactics = Theory_Data
(
type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
val empty = [];
- val copy = I;
val extend = I;
- fun merge _ = AList.merge (op =) (K true);
+ fun merge data : T = AList.merge (op =) (K true) data;
);
fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
--- a/src/HOL/Tools/inductive_codegen.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Sun Nov 08 18:43:42 2009 +0100
@@ -20,7 +20,7 @@
fun merge_rules tabs =
Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
-structure CodegenData = TheoryDataFun
+structure CodegenData = Theory_Data
(
type T =
{intros : (thm * (string * int)) list Symtab.table,
@@ -28,10 +28,9 @@
eqns : (thm * string) list Symtab.table};
val empty =
{intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
- val copy = I;
val extend = I;
- fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1},
- {intros=intros2, graph=graph2, eqns=eqns2}) =
+ fun merge ({intros=intros1, graph=graph1, eqns=eqns1},
+ {intros=intros2, graph=graph2, eqns=eqns2}) : T =
{intros = merge_rules (intros1, intros2),
graph = Graph.merge (K true) (graph1, graph2),
eqns = merge_rules (eqns1, eqns2)};
--- a/src/HOL/Tools/recdef.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/recdef.ML Sun Nov 08 18:43:42 2009 +0100
@@ -86,18 +86,17 @@
type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
-structure GlobalRecdefData = TheoryDataFun
+structure GlobalRecdefData = Theory_Data
(
type T = recdef_info Symtab.table * hints;
val empty = (Symtab.empty, mk_hints ([], [], [])): T;
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
(tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
(Symtab.merge (K true) (tab1, tab2),
mk_hints (Thm.merge_thms (simps1, simps2),
- AList.merge (op =) Thm.eq_thm (congs1, congs2),
+ AList.merge (op =) Thm.eq_thm_prop (congs1, congs2),
Thm.merge_thms (wfs1, wfs2)));
);
--- a/src/HOL/Tools/recfun_codegen.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Sun Nov 08 18:43:42 2009 +0100
@@ -16,13 +16,12 @@
val const_of = dest_Const o head_of o fst o Logic.dest_equals;
-structure ModuleData = TheoryDataFun
+structure ModuleData = Theory_Data
(
type T = string Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (K true);
+ fun merge data = Symtab.merge (K true) data;
);
fun add_thm_target module_name thm thy =
--- a/src/HOL/Tools/record.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/record.ML Sun Nov 08 18:43:42 2009 +0100
@@ -81,13 +81,12 @@
cterm_instantiate (map (apfst getvar) values) thm
end;
-structure IsTupleThms = TheoryDataFun
+structure IsTupleThms = Theory_Data
(
type T = thm Symtab.table;
val empty = Symtab.make [tuple_istuple];
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge Thm.eq_thm_prop;
+ fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *)
);
fun do_typedef name repT alphas thy =
@@ -381,7 +380,7 @@
equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
extfields = extfields, fieldext = fieldext }: record_data;
-structure RecordsData = TheoryDataFun
+structure RecordsData = Theory_Data
(
type T = record_data;
val empty =
@@ -390,10 +389,8 @@
simpset = HOL_basic_ss, defset = HOL_basic_ss,
foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
-
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
({records = recs1,
sel_upd =
{selectors = sels1, updates = upds1,
@@ -425,7 +422,7 @@
foldcong = Simplifier.merge_ss (fc1, fc2),
unfoldcong = Simplifier.merge_ss (uc1, uc2)}
(Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
- (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2))
+ (Thm.merge_thms (extinjects1, extinjects2))
(Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
(Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
--- a/src/HOL/Tools/refute.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/refute.ML Sun Nov 08 18:43:42 2009 +0100
@@ -201,7 +201,7 @@
};
- structure RefuteData = TheoryDataFun
+ structure RefuteData = Theory_Data
(
type T =
{interpreters: (string * (theory -> model -> arguments -> term ->
@@ -210,11 +210,10 @@
(int -> bool) -> term option)) list,
parameters: string Symtab.table};
val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
({interpreters = in1, printers = pr1, parameters = pa1},
- {interpreters = in2, printers = pr2, parameters = pa2}) =
+ {interpreters = in2, printers = pr2, parameters = pa2}) : T =
{interpreters = AList.merge (op =) (K true) (in1, in2),
printers = AList.merge (op =) (K true) (pr1, pr2),
parameters = Symtab.merge (op=) (pa1, pa2)};
--- a/src/HOL/Tools/res_axioms.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Sun Nov 08 18:43:42 2009 +0100
@@ -349,13 +349,12 @@
(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
Skolem functions.*)
-structure ThmCache = TheoryDataFun
+structure ThmCache = Theory_Data
(
type T = thm list Thmtab.table * unit Symtab.table;
val empty = (Thmtab.empty, Symtab.empty);
- val copy = I;
val extend = I;
- fun merge _ ((cache1, seen1), (cache2, seen2)) : T =
+ fun merge ((cache1, seen1), (cache2, seen2)) : T =
(Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
);
--- a/src/HOL/Tools/typecopy.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/typecopy.ML Sun Nov 08 18:43:42 2009 +0100
@@ -30,13 +30,12 @@
proj_def: thm
};
-structure TypecopyData = TheoryDataFun
+structure TypecopyData = Theory_Data
(
type T = info Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (K true);
+ fun merge data = Symtab.merge (K true) data;
);
val get_info = Symtab.lookup o TypecopyData.get;
--- a/src/HOL/Tools/typedef.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/typedef.ML Sun Nov 08 18:43:42 2009 +0100
@@ -36,13 +36,12 @@
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
Rep_induct: thm, Abs_induct: thm};
-structure TypedefData = TheoryDataFun
+structure TypedefData = Theory_Data
(
type T = info Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (K true) tabs;
+ fun merge data = Symtab.merge (K true) data;
);
val get_info = Symtab.lookup o TypedefData.get;
--- a/src/HOLCF/Tools/fixrec.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML Sun Nov 08 18:43:42 2009 +0100
@@ -252,12 +252,12 @@
(*********** monadic notation and pattern matching compilation ***********)
(*************************************************************************)
-structure FixrecMatchData = TheoryDataFun (
+structure FixrecMatchData = Theory_Data
+(
type T = string Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (K true);
+ fun merge data = Symtab.merge (K true) data;
);
(* associate match functions with pattern constants *)
@@ -523,8 +523,7 @@
end;
val setup =
- FixrecMatchData.init
- #> Attrib.setup @{binding fixrec_simp}
+ Attrib.setup @{binding fixrec_simp}
(Attrib.add_del fixrec_simp_add fixrec_simp_del)
"declaration of fixrec simp rule"
#> Method.setup @{binding fixrec_simp}
--- a/src/Provers/classical.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Provers/classical.ML Sun Nov 08 18:43:42 2009 +0100
@@ -835,13 +835,12 @@
(* global clasets *)
-structure GlobalClaset = TheoryDataFun
+structure GlobalClaset = Theory_Data
(
type T = claset * context_cs;
val empty = (empty_cs, empty_context_cs);
- val copy = I;
val extend = I;
- fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
+ fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
(merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
);
--- a/src/Pure/Isar/attrib.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Sun Nov 08 18:43:42 2009 +0100
@@ -65,13 +65,12 @@
(* theory data *)
-structure Attributes = TheoryDataFun
+structure Attributes = Theory_Data
(
type T = ((src -> attribute) * string) Name_Space.table;
val empty : T = Name_Space.empty_table "attribute";
- val copy = I;
val extend = I;
- fun merge _ tables : T = Name_Space.merge_tables tables;
+ fun merge data : T = Name_Space.merge_tables data;
);
fun print_attributes thy =
@@ -321,13 +320,12 @@
(* naming *)
-structure Configs = TheoryDataFun
+structure Configs = Theory_Data
(
type T = Config.value Config.T Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ = Symtab.merge (K true);
+ fun merge data = Symtab.merge (K true) data;
);
fun print_configs ctxt =
--- a/src/Pure/Isar/class_target.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Sun Nov 08 18:43:42 2009 +0100
@@ -105,13 +105,12 @@
(Thm.merge_thms (defs1, defs2),
AList.merge (op =) (K true) (operations1, operations2)));
-structure ClassData = TheoryDataFun
+structure ClassData = Theory_Data
(
type T = class_data Graph.T
val empty = Graph.empty;
- val copy = I;
val extend = I;
- fun merge _ = Graph.join merge_class_data;
+ val merge = Graph.join merge_class_data;
);
--- a/src/Pure/Isar/code.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/code.ML Sun Nov 08 18:43:42 2009 +0100
@@ -703,13 +703,12 @@
(* c.f. src/HOL/Tools/recfun_codegen.ML *)
-structure Code_Target_Attr = TheoryDataFun (
+structure Code_Target_Attr = Theory_Data
+(
type T = (string -> thm -> theory -> theory) option;
val empty = NONE;
- val copy = I;
val extend = I;
- fun merge _ (NONE, f2) = f2
- | merge _ (f1, _) = f1;
+ fun merge (f1, f2) = if is_some f1 then f1 else f2;
);
fun set_code_target_attr f = Code_Target_Attr.map (K (SOME f));
--- a/src/Pure/Isar/locale.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/locale.ML Sun Nov 08 18:43:42 2009 +0100
@@ -122,13 +122,12 @@
merge (eq_snd op =) (notes, notes')),
merge (eq_snd op =) (dependencies, dependencies')));
-structure Locales = TheoryDataFun
+structure Locales = Theory_Data
(
type T = locale Name_Space.table;
val empty : T = Name_Space.empty_table "locale";
- val copy = I;
val extend = I;
- fun merge _ = Name_Space.join_tables (K merge_locale);
+ val merge = Name_Space.join_tables (K merge_locale);
);
val intern = Name_Space.intern o #1 o Locales.get;
@@ -332,7 +331,7 @@
(*** Registrations: interpretations in theories ***)
-structure Registrations = TheoryDataFun
+structure Registrations = Theory_Data
(
type T = ((string * (morphism * morphism)) * stamp) list *
(* registrations, in reverse order of declaration *)
@@ -340,8 +339,7 @@
(* alist of mixin lists, per list mixins in reverse order of declaration *)
val empty = ([], []);
val extend = I;
- val copy = I;
- fun merge _ ((r1, m1), (r2, m2)) : T =
+ fun merge ((r1, m1), (r2, m2)) : T =
(Library.merge (eq_snd op =) (r1, r2),
AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
(* FIXME consolidate with dependencies, consider one data slot only *)
--- a/src/Pure/Isar/method.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/method.ML Sun Nov 08 18:43:42 2009 +0100
@@ -320,13 +320,12 @@
(* method definitions *)
-structure Methods = TheoryDataFun
+structure Methods = Theory_Data
(
type T = ((src -> Proof.context -> method) * string) Name_Space.table;
val empty : T = Name_Space.empty_table "method";
- val copy = I;
val extend = I;
- fun merge _ tables : T = Name_Space.merge_tables tables;
+ fun merge data : T = Name_Space.merge_tables data;
);
fun print_methods thy =
--- a/src/Pure/Isar/object_logic.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/object_logic.ML Sun Nov 08 18:43:42 2009 +0100
@@ -47,18 +47,17 @@
fun make_data (base_sort, judgment, atomize_rulify) =
Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
-structure ObjectLogicData = TheoryDataFun
+structure ObjectLogicData = Theory_Data
(
type T = data;
val empty = make_data (NONE, NONE, ([], []));
- val copy = I;
val extend = I;
fun merge_opt eq (SOME x, SOME y) =
if eq (x, y) then SOME x else error "Attempt to merge different object-logics"
| merge_opt _ (x, y) = if is_some x then x else y;
- fun merge _
+ fun merge
(Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)},
Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) =
make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2),
--- a/src/Pure/Proof/extraction.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Sun Nov 08 18:43:42 2009 +0100
@@ -167,7 +167,7 @@
(* theory data *)
-structure ExtractionData = TheoryDataFun
+structure ExtractionData = Theory_Data
(
type T =
{realizes_eqns : rules,
@@ -187,20 +187,19 @@
defs = [],
expand = [],
prep = NONE};
- val copy = I;
val extend = I;
- fun merge _
- (({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
+ fun merge
+ ({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
realizers = realizers1, defs = defs1, expand = expand1, prep = prep1},
{realizes_eqns = realizes_eqns2, typeof_eqns = typeof_eqns2, types = types2,
- realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T * T) =
+ realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T =
{realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
types = AList.merge (op =) (K true) (types1, types2),
realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
defs = Library.merge Thm.eq_thm (defs1, defs2),
- expand = Library.merge (op =) (expand1, expand2),
+ expand = Library.merge (op =) (expand1, expand2), (* FIXME proper aconv !?! *)
prep = (case prep1 of NONE => prep2 | _ => prep1)};
);
--- a/src/Pure/Thy/present.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Thy/present.ML Sun Nov 08 18:43:42 2009 +0100
@@ -64,13 +64,12 @@
(** additional theory data **)
-structure BrowserInfoData = TheoryDataFun
+structure BrowserInfoData = Theory_Data
(
type T = {name: string, session: string list, is_local: bool};
val empty = {name = "", session = [], is_local = false}: T;
- val copy = I;
fun extend _ = empty;
- fun merge _ _ = empty;
+ fun merge _ = empty;
);
val put_info = BrowserInfoData.put;
--- a/src/Pure/Thy/term_style.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Thy/term_style.ML Sun Nov 08 18:43:42 2009 +0100
@@ -19,13 +19,12 @@
fun err_dup_style name =
error ("Duplicate declaration of antiquote style: " ^ quote name);
-structure StyleData = TheoryDataFun
+structure StyleData = Theory_Data
(
type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
+ fun merge data : T = Symtab.merge (eq_snd (op =)) data
handle Symtab.DUP dup => err_dup_style dup;
);
--- a/src/Pure/Thy/thy_info.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML Sun Nov 08 18:43:42 2009 +0100
@@ -233,15 +233,14 @@
(* management data *)
-structure Management_Data = TheoryDataFun
+structure Management_Data = Theory_Data
(
type T =
Task_Queue.group option * (*worker thread group*)
int; (*abstract update time*)
val empty = (NONE, 0);
- val copy = I;
fun extend _ = empty;
- fun merge _ _ = empty;
+ fun merge _ = empty;
);
val thy_ord = int_ord o pairself (#2 o Management_Data.get);
--- a/src/Pure/codegen.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/codegen.ML Sun Nov 08 18:43:42 2009 +0100
@@ -185,7 +185,7 @@
(* theory data *)
-structure CodegenData = TheoryDataFun
+structure CodegenData = Theory_Data
(
type T =
{codegens : (string * term codegen) list,
@@ -198,16 +198,15 @@
val empty =
{codegens = [], tycodegens = [], consts = [], types = [],
preprocs = [], modules = Symtab.empty};
- val copy = I;
val extend = I;
- fun merge _
+ fun merge
({codegens = codegens1, tycodegens = tycodegens1,
consts = consts1, types = types1,
preprocs = preprocs1, modules = modules1} : T,
{codegens = codegens2, tycodegens = tycodegens2,
consts = consts2, types = types2,
- preprocs = preprocs2, modules = modules2}) =
+ preprocs = preprocs2, modules = modules2}) : T =
{codegens = AList.merge (op =) (K true) (codegens1, codegens2),
tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
consts = AList.merge (op =) (K true) (consts1, consts2),
@@ -287,13 +286,12 @@
| _ => err ()
end;
-structure UnfoldData = TheoryDataFun
+structure UnfoldData = Theory_Data
(
type T = simpset;
val empty = empty_ss;
- val copy = I;
val extend = I;
- fun merge _ = merge_ss;
+ val merge = merge_ss;
);
val map_unfold = UnfoldData.map;
--- a/src/Pure/interpretation.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/interpretation.ML Sun Nov 08 18:43:42 2009 +0100
@@ -18,13 +18,12 @@
type T = T;
-structure Interp = TheoryDataFun
+structure Interp = Theory_Data
(
type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
val empty = ([], []);
val extend = I;
- val copy = I;
- fun merge _ ((data1, interps1), (data2, interps2)) : T =
+ fun merge ((data1, interps1), (data2, interps2)) : T =
(Library.merge eq (data1, data2),
AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
);
--- a/src/Pure/proofterm.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/proofterm.ML Sun Nov 08 18:43:42 2009 +0100
@@ -1247,14 +1247,13 @@
(**** theory data ****)
-structure ProofData = TheoryDataFun
+structure ProofData = Theory_Data
(
type T = (stamp * (proof * proof)) list * (stamp * (typ list -> proof -> proof option)) list;
val empty = ([], []);
- val copy = I;
val extend = I;
- fun merge _ ((rules1, procs1), (rules2, procs2)) : T =
+ fun merge ((rules1, procs1), (rules2, procs2)) : T =
(AList.merge (op =) (K true) (rules1, rules2),
AList.merge (op =) (K true) (procs1, procs2));
);
--- a/src/Pure/pure_thy.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/pure_thy.ML Sun Nov 08 18:43:42 2009 +0100
@@ -54,13 +54,12 @@
(** theory data **)
-structure FactsData = TheoryDataFun
+structure FactsData = Theory_Data
(
type T = Facts.T * thm list;
val empty = (Facts.empty, []);
- val copy = I;
fun extend (facts, _) = (facts, []);
- fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
+ fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
);
@@ -246,13 +245,12 @@
("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
-structure OldApplSyntax = TheoryDataFun
+structure OldApplSyntax = Theory_Data
(
type T = bool;
val empty = false;
- val copy = I;
val extend = I;
- fun merge _ (b1, b2) : T =
+ fun merge (b1, b2) : T =
if b1 = b2 then b1
else error "Cannot merge theories with different application syntax";
);
@@ -269,7 +267,7 @@
val _ = Context.>> (Context.map_theory
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
- OldApplSyntax.init #>
+ OldApplSyntax.put false #>
Sign.add_types
[(Binding.name "fun", 2, NoSyn),
(Binding.name "prop", 0, NoSyn),
--- a/src/Pure/thm.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/thm.ML Sun Nov 08 18:43:42 2009 +0100
@@ -1724,13 +1724,12 @@
(* authentic derivation names *)
-structure Oracles = TheoryDataFun
+structure Oracles = Theory_Data
(
type T = unit Name_Space.table;
val empty : T = Name_Space.empty_table "oracle";
- val copy = I;
val extend = I;
- fun merge _ oracles : T = Name_Space.merge_tables oracles;
+ fun merge data : T = Name_Space.merge_tables data;
);
val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
--- a/src/Tools/Code/code_preproc.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Tools/Code/code_preproc.ML Sun Nov 08 18:43:42 2009 +0100
@@ -56,13 +56,12 @@
val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
in make_thmproc ((pre, post), functrans) end;
-structure Code_Preproc_Data = TheoryDataFun
+structure Code_Preproc_Data = Theory_Data
(
type T = thmproc;
val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
- fun copy spec = spec;
- val extend = copy;
- fun merge _ = merge_thmproc;
+ val extend = I;
+ val merge = merge_thmproc;
);
fun the_thmproc thy = case Code_Preproc_Data.get thy
--- a/src/Tools/Code/code_target.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Tools/Code/code_target.ML Sun Nov 08 18:43:42 2009 +0100
@@ -148,13 +148,12 @@
else
error ("Incompatible serializers: " ^ quote target);
-structure CodeTargetData = TheoryDataFun
+structure CodeTargetData = Theory_Data
(
type T = target Symtab.table * string list;
val empty = (Symtab.empty, []);
- val copy = I;
val extend = I;
- fun merge _ ((target1, exc1) : T, (target2, exc2)) =
+ fun merge ((target1, exc1), (target2, exc2)) : T =
(Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
);
--- a/src/Tools/nbe.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Tools/nbe.ML Sun Nov 08 18:43:42 2009 +0100
@@ -37,13 +37,12 @@
(** certificates and oracle for "trivial type classes" **)
-structure Triv_Class_Data = TheoryDataFun
+structure Triv_Class_Data = Theory_Data
(
type T = (class * thm) list;
val empty = [];
- val copy = I;
val extend = I;
- fun merge pp = AList.merge (op =) (K true);
+ fun merge data : T = AList.merge (op =) (K true) data;
);
fun add_const_alias thm thy =
--- a/src/Tools/quickcheck.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Tools/quickcheck.ML Sun Nov 08 18:43:42 2009 +0100
@@ -52,16 +52,16 @@
make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
case default_type1 of NONE => default_type2 | _ => default_type1);
-structure Data = TheoryDataFun(
+structure Data = Theory_Data
+(
type T = (string * (Proof.context -> term -> int -> term list option)) list
* test_params;
val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE });
- val copy = I;
val extend = I;
- fun merge pp ((generators1, params1), (generators2, params2)) =
- (AList.merge (op = : string * string -> bool) (K true) (generators1, generators2),
+ fun merge ((generators1, params1), (generators2, params2)) : T =
+ (AList.merge (op =) (K true) (generators1, generators2),
merge_test_params (params1, params2));
-)
+);
val add_generator = Data.map o apfst o AList.update (op =);
--- a/src/Tools/value.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Tools/value.ML Sun Nov 08 18:43:42 2009 +0100
@@ -15,12 +15,12 @@
structure Value : VALUE =
struct
-structure Evaluator = TheoryDataFun(
+structure Evaluator = Theory_Data
+(
type T = (string * (Proof.context -> term -> term)) list;
val empty = [];
- val copy = I;
val extend = I;
- fun merge _ data = AList.merge (op =) (K true) data;
+ fun merge data : T = AList.merge (op =) (K true) data;
)
val add_evaluator = Evaluator.map o AList.update (op =);
--- a/src/ZF/Tools/ind_cases.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/ZF/Tools/ind_cases.ML Sun Nov 08 18:43:42 2009 +0100
@@ -18,13 +18,12 @@
(* theory data *)
-structure IndCasesData = TheoryDataFun
+structure IndCasesData = Theory_Data
(
type T = (simpset -> cterm -> thm) Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (K true) tabs;
+ fun merge data = Symtab.merge (K true) data;
);
--- a/src/ZF/Tools/induct_tacs.ML Sun Nov 08 18:43:22 2009 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Sun Nov 08 18:43:42 2009 +0100
@@ -29,13 +29,12 @@
mutual_induct : thm,
exhaustion : thm};
-structure DatatypesData = TheoryDataFun
+structure DatatypesData = Theory_Data
(
type T = datatype_info Symtab.table;
val empty = Symtab.empty;
- val copy = I;
val extend = I;
- fun merge _ tabs : T = Symtab.merge (K true) tabs;
+ fun merge data : T = Symtab.merge (K true) data;
);
@@ -49,13 +48,12 @@
rec_rewrites : thm list}; (*recursor equations*)
-structure ConstructorsData = TheoryDataFun
+structure ConstructorsData = Theory_Data
(
type T = constructor_info Symtab.table
val empty = Symtab.empty
- val copy = I;
val extend = I
- fun merge _ tabs : T = Symtab.merge (K true) tabs;
+ fun merge data = Symtab.merge (K true) data;
);
structure DatatypeTactics : DATATYPE_TACTICS =