--- a/NEWS Wed Oct 20 17:11:46 2021 +0200
+++ b/NEWS Wed Oct 20 18:13:17 2021 +0200
@@ -37,6 +37,9 @@
now work uniformly in Isabelle/Haskell vs. Isabelle/ML vs.
Isabelle/Scala/PIDE.
+* Theory_Data / Generic_Data: "val extend = I" has been removed;
+obsolete since Isabelle2021.
+
*** Isar ***
--- a/src/Doc/Implementation/Prelim.thy Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Doc/Implementation/Prelim.thy Wed Oct 20 18:13:17 2021 +0200
@@ -380,7 +380,6 @@
(
type T = term Ord_List.T;
val empty = [];
- val extend = I;
fun merge (ts1, ts2) =
Ord_List.union Term_Ord.fast_term_ord ts1 ts2;
);
--- a/src/HOL/Algebra/ringsimp.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Wed Oct 20 18:13:17 2021 +0200
@@ -26,7 +26,6 @@
identifier of the structure, list of operations and simp rules,
identifier and operations identify the structure uniquely. *)
val empty = [];
- val extend = I;
val merge = AList.join struct_eq (K Thm.merge_thms);
);
--- a/src/HOL/Analysis/measurable.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Analysis/measurable.ML Wed Oct 20 18:13:17 2021 +0200
@@ -56,7 +56,6 @@
dest_thms = Thm.item_net,
cong_thms = Thm.item_net,
preprocessors = [] };
- val extend = I;
fun merge ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1 },
{measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) : T = {
measurable_thms = Item_Net.merge (t1, t2),
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy Wed Oct 20 18:13:17 2021 +0200
@@ -720,7 +720,6 @@
(struct
type T = (term * (thm list * thm list * thm list * thm list * thm * thm)) Net.net
val empty = Net.empty
- val extend = I
val merge = Net.merge eq_ring_simps
end);
--- a/src/HOL/Decision_Procs/Reflective_Field.thy Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy Wed Oct 20 18:13:17 2021 +0200
@@ -737,7 +737,6 @@
(struct
type T = (term * (thm list * thm list * thm list * thm * thm)) Net.net
val empty = Net.empty
- val extend = I
val merge = Net.merge eq_field_simps
end);
--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Wed Oct 20 18:13:17 2021 +0200
@@ -40,7 +40,6 @@
(
type T = (thm * entry) list;
val empty = [];
- val extend = I;
fun merge data : T = AList.merge eq_key (K true) data;
);
--- a/src/HOL/Decision_Procs/langford_data.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Decision_Procs/langford_data.ML Wed Oct 20 18:13:17 2021 +0200
@@ -23,7 +23,6 @@
(
type T = simpset * (thm * entry) list;
val empty = (HOL_basic_ss, []);
- val extend = I;
fun merge ((ss1, es1), (ss2, es2)) : T =
(merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2));
);
--- a/src/HOL/Eisbach/Tests.thy Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Eisbach/Tests.thy Wed Oct 20 18:13:17 2021 +0200
@@ -417,7 +417,6 @@
(
type T = thm list;
val empty: T = [];
- val extend = I;
fun merge data : T = Thm.merge_thms data;
);
\<close>
--- a/src/HOL/Eisbach/method_closure.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Wed Oct 20 18:13:17 2021 +0200
@@ -54,7 +54,6 @@
(
type T = closure Symtab.table;
val empty: T = Symtab.empty;
- val extend = I;
fun merge data : T = Symtab.merge (K true) data;
);
--- a/src/HOL/HOL.thy Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/HOL.thy Wed Oct 20 18:13:17 2021 +0200
@@ -1658,7 +1658,6 @@
(
type T = ((term -> bool) * stamp) list;
val empty = [];
- val extend = I;
fun merge data : T = Library.merge (eq_snd (op =)) data;
);
fun add m = Data.map (cons (m, stamp ()));
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Oct 20 18:13:17 2021 +0200
@@ -119,7 +119,6 @@
(* list indicates which type arguments allow indirect recursion *)
type T = (bool list) Symtab.table
val empty = Symtab.empty
- val extend = I
fun merge data = Symtab.merge (K true) data
)
--- a/src/HOL/HOLCF/Tools/fixrec.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Wed Oct 20 18:13:17 2021 +0200
@@ -88,7 +88,6 @@
(
type T = thm Symtab.table
val empty = Symtab.empty
- val extend = I
fun merge data : T = Symtab.merge (K true) data
)
@@ -190,7 +189,6 @@
(
type T = string Symtab.table
val empty = Symtab.empty
- val extend = I
fun merge data = Symtab.merge (K true) data
)
--- a/src/HOL/Hoare/hoare_syntax.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Hoare/hoare_syntax.ML Wed Oct 20 18:13:17 2021 +0200
@@ -27,7 +27,6 @@
{Basic: string, Skip: string, Seq: string, Cond: string, While: string,
Valid: string, ValidTC: string} option;
val empty: T = NONE;
- val extend = I;
fun merge (data1, data2) =
if is_some data1 andalso is_some data2 andalso data1 <> data2 then
error "Cannot merge syntax from different Hoare Logics"
--- a/src/HOL/Import/import_data.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Import/import_data.ML Wed Oct 20 18:13:17 2021 +0200
@@ -29,7 +29,6 @@
const_def: thm Symtab.table, ty_def: thm Symtab.table}
val empty = {const_map = Symtab.empty, ty_map = Symtab.empty,
const_def = Symtab.empty, ty_def = Symtab.empty}
- val extend = I
fun merge
({const_map = cm1, ty_map = tm1, const_def = cd1, ty_def = td1},
{const_map = cm2, ty_map = tm2, const_def = cd2, ty_def = td2}) : T =
--- a/src/HOL/Library/adhoc_overloading.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Library/adhoc_overloading.ML Wed Oct 20 18:13:17 2021 +0200
@@ -65,7 +65,6 @@
{variants : (term * typ) list Symtab.table,
oconsts : string Termtab.table};
val empty = {variants = Symtab.empty, oconsts = Termtab.empty};
- val extend = I;
fun merge
({variants = vtab1, oconsts = otab1},
--- a/src/HOL/Library/code_lazy.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML Wed Oct 20 18:13:17 2021 +0200
@@ -56,7 +56,6 @@
type T = lazy_info Symtab.table;
val empty = Symtab.empty;
val merge = Symtab.join (fn _ => fn (_, record) => record);
- val extend = I;
);
fun fold_type type' tfree tvar typ =
--- a/src/HOL/Library/code_test.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Library/code_test.ML Wed Oct 20 18:13:17 2021 +0200
@@ -70,7 +70,6 @@
type T =
(string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list
val empty = []
- val extend = I
fun merge data : T = AList.merge (op =) (K true) data
)
--- a/src/HOL/Library/datatype_records.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Library/datatype_records.ML Wed Oct 20 18:13:17 2021 +0200
@@ -32,7 +32,6 @@
type T = data
val empty = Symtab.empty
val merge = Symtab.merge op =
- val extend = I
)
fun mk_eq_dummy (lhs, rhs) =
--- a/src/HOL/Library/old_recdef.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Library/old_recdef.ML Wed Oct 20 18:13:17 2021 +0200
@@ -2739,7 +2739,6 @@
(
type T = recdef_info Symtab.table * hints;
val empty = (Symtab.empty, mk_hints ([], [], [])): T;
- val extend = I;
fun merge
((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
(tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
--- a/src/HOL/Library/refute.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Library/refute.ML Wed Oct 20 18:13:17 2021 +0200
@@ -192,7 +192,6 @@
(int -> bool) -> term option)) list,
parameters: string Symtab.table};
val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
- val extend = I;
fun merge
({interpreters = in1, printers = pr1, parameters = pa1},
{interpreters = in2, printers = pr2, parameters = pa2}) : T =
--- a/src/HOL/Nominal/nominal_atoms.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Oct 20 18:13:17 2021 +0200
@@ -46,7 +46,6 @@
(
type T = atom_info Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data = Symtab.merge (K true) data;
);
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Oct 20 18:13:17 2021 +0200
@@ -55,7 +55,6 @@
(
type T = nominal_datatype_info Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data = Symtab.merge (K true) data;
);
--- a/src/HOL/Nominal/nominal_thmdecls.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Wed Oct 20 18:13:17 2021 +0200
@@ -28,7 +28,6 @@
(
type T = thm list
val empty = []
- val extend = I
val merge = Thm.merge_thms
)
--- a/src/HOL/Nonstandard_Analysis/transfer_principle.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Nonstandard_Analysis/transfer_principle.ML Wed Oct 20 18:13:17 2021 +0200
@@ -22,7 +22,6 @@
consts: string list
};
val empty = {intros = [], unfolds = [], refolds = [], consts = []};
- val extend = I;
fun merge
({intros = intros1, unfolds = unfolds1,
refolds = refolds1, consts = consts1},
--- a/src/HOL/Real_Asymp/exp_log_expression.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML Wed Oct 20 18:13:17 2021 +0200
@@ -135,7 +135,6 @@
fun merge ({name_table = tbl1, net = net1}, {name_table = tbl2, net = net2}) =
{name_table = Name_Space.join_tables (fn _ => raise DUP) (tbl1, tbl2),
net = Item_Net.merge (net1, net2)}
- val extend = I
)
fun rewrite' ctxt old_prems bounds thms ct =
--- a/src/HOL/Real_Asymp/multiseries_expansion.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Real_Asymp/multiseries_expansion.ML Wed Oct 20 18:13:17 2021 +0200
@@ -136,7 +136,6 @@
(
type T = (Proof.context -> int -> tactic) Name_Space.table;
val empty : T = Name_Space.empty_table "sign_oracle_tactic";
- val extend = I;
fun merge (tactics1, tactics2) : T = Name_Space.merge_tables (tactics1, tactics2);
);
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Wed Oct 20 18:13:17 2021 +0200
@@ -58,7 +58,6 @@
path: Path.T,
prefix: string} option}
val empty : T = {pfuns = Symtab.empty, type_map = Symtab.empty, env = NONE}
- val extend = I
fun merge ({pfuns = pfuns1, type_map = type_map1, env = NONE},
{pfuns = pfuns2, type_map = type_map2, env = NONE}) =
{pfuns = Symtab.merge (eq_pair (op =) (op aconv)) (pfuns1, pfuns2),
--- a/src/HOL/Statespace/state_fun.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Statespace/state_fun.ML Wed Oct 20 18:13:17 2021 +0200
@@ -101,7 +101,6 @@
(
type T = simpset * simpset * bool; (*lookup simpset, ex_lookup simpset, are simprocs installed*)
val empty = (empty_ss, empty_ss, false);
- val extend = I;
fun merge ((ss1, ex_ss1, b1), (ss2, ex_ss2, b2)) =
(merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
);
--- a/src/HOL/Statespace/state_space.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Oct 20 18:13:17 2021 +0200
@@ -95,7 +95,6 @@
(
type T = namespace_info;
val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false};
- val extend = I;
fun merge
({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
{declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T =
@@ -156,7 +155,6 @@
(
type T = statespace_info Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data : T = Symtab.merge (K true) data;
);
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Oct 20 18:13:17 2021 +0200
@@ -146,7 +146,6 @@
(
type T = manifest list
val empty = []
- val extend = I
fun merge data : T = Library.merge (op =) data
)
val get_manifests = TPTP_Data.get
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Wed Oct 20 18:13:17 2021 +0200
@@ -156,7 +156,6 @@
(
type T = manifest list
val empty = []
- val extend = I
fun merge data : T = Library.merge manifest_eq data
)
val get_manifests : theory -> manifest list = TPTP_Reconstruction_Data.get
@@ -207,7 +206,6 @@
(
type T = tptp_reconstruction_state
val empty = {next_int = 0}
- val extend = I
fun merge data : T = snd data
)
--- a/src/HOL/Tools/Argo/argo_tactic.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Argo/argo_tactic.ML Wed Oct 20 18:13:17 2021 +0200
@@ -105,7 +105,6 @@
(
type T = (serial * extension) list
val empty = []
- val extend = I
val merge = merge eq_extension
)
--- a/src/HOL/Tools/BNF/bnf_def.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Oct 20 18:13:17 2021 +0200
@@ -670,7 +670,6 @@
(
type T = bnf Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data : T = Symtab.merge (K true) data;
);
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Oct 20 18:13:17 2021 +0200
@@ -393,7 +393,6 @@
(
type T = fp_sugar Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data : T = Symtab.merge (K true) data;
);
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Oct 20 18:13:17 2021 +0200
@@ -44,7 +44,6 @@
(
type T = n2m_sugar Typtab.table;
val empty = Typtab.empty;
- val extend = I;
fun merge data : T = Typtab.merge (K true) data;
);
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Wed Oct 20 18:13:17 2021 +0200
@@ -406,7 +406,6 @@
(
type T = corec_data;
val empty = (Symtab.empty, [Symtab.empty]);
- val extend = I;
fun merge ((version_tab1, info_tabs1), (version_tab2, info_tabs2)) : T =
(Symtab.join (K Int.max) (version_tab1, version_tab2), info_tabs1 @ info_tabs2);
);
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Wed Oct 20 18:13:17 2021 +0200
@@ -137,7 +137,6 @@
(
type T = corec_sugar_data;
val empty = (Symtab.empty, Symtab.empty, Symtab.empty);
- val extend = I;
fun merge data : T =
(Symtab.merge (K true) (apply2 #1 data), Symtab.merge (K true) (apply2 #2 data),
Symtab.join (K merge_friend_extras) (apply2 #3 data));
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Oct 20 18:13:17 2021 +0200
@@ -143,7 +143,6 @@
(
type T = lfp_rec_extension option;
val empty = NONE;
- val extend = I;
val merge = merge_options;
);
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Oct 20 18:13:17 2021 +0200
@@ -44,7 +44,6 @@
(
type T = (string * (thm * thm list * thm list)) Symtab.table;
val empty = Symtab.empty;
- val extend = I
fun merge data = Symtab.merge (K true) data;
);
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Wed Oct 20 18:13:17 2021 +0200
@@ -65,7 +65,6 @@
(
type T = data;
val empty = make_data (Symtab.empty, Symtab.empty);
- val extend = I;
fun merge
(Data {constrs = constrs1, cases = cases1},
Data {constrs = constrs2, cases = cases2}) =
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Oct 20 18:13:17 2021 +0200
@@ -179,7 +179,6 @@
(
type T = (Position.T * ctr_sugar) Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data : T = Symtab.merge (K true) data;
);
--- a/src/HOL/Tools/Function/function_common.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Wed Oct 20 18:13:17 2021 +0200
@@ -258,7 +258,6 @@
Item_Net.init (op aconv o apply2 fst) (single o fst),
fn _ => error "Termination prover not configured",
empty_preproc check_defs)
- val extend = I
fun merge
((termination_rules1, functions1, termination_prover1, preproc1),
(termination_rules2, functions2, _, _)) : T =
--- a/src/HOL/Tools/Function/function_context_tree.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Function/function_context_tree.ML Wed Oct 20 18:13:17 2021 +0200
@@ -47,7 +47,6 @@
(
type T = thm list
val empty = []
- val extend = I
val merge = Thm.merge_thms
);
--- a/src/HOL/Tools/Function/partial_function.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Wed Oct 20 18:13:17 2021 +0200
@@ -44,7 +44,6 @@
(
type T = setup_data Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data = Symtab.merge (K true) data;
)
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Wed Oct 20 18:13:17 2021 +0200
@@ -63,7 +63,6 @@
(
type T = multiset_setup option
val empty = NONE
- val extend = I;
val merge = merge_options
)
--- a/src/HOL/Tools/Lifting/lifting_def.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed Oct 20 18:13:17 2021 +0200
@@ -514,7 +514,6 @@
(
type T = code_eq option
val empty = NONE
- val extend = I
fun merge _ = NONE
);
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Oct 20 18:13:17 2021 +0200
@@ -110,7 +110,6 @@
(
type T = code_dt Item_Net.T
val empty = Item_Net.init code_dt_eq term_of_code_dt
- val extend = I
val merge = Item_Net.merge
);
--- a/src/HOL/Tools/Lifting/lifting_info.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Wed Oct 20 18:13:17 2021 +0200
@@ -92,7 +92,6 @@
restore_data = Symtab.empty,
no_code_types = Symtab.empty
}
- val extend = I
fun merge
( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1,
restore_data = rd1, no_code_types = nct1 },
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Wed Oct 20 18:13:17 2021 +0200
@@ -130,7 +130,6 @@
(
type T = raw_param list
val empty = default_default_params |> map (apsnd single)
- val extend = I
fun merge data = AList.merge (op =) (K true) data
)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Oct 20 18:13:17 2021 +0200
@@ -288,7 +288,6 @@
ersatz_table: (string * string) list,
codatatypes: (string * (string * (string * typ) list)) list}
val empty = {frac_types = [], ersatz_table = [], codatatypes = []}
- val extend = I
fun merge ({frac_types = fs1, ersatz_table = et1, codatatypes = cs1},
{frac_types = fs2, ersatz_table = et2, codatatypes = cs2}) : T =
{frac_types = AList.merge (op =) (K true) (fs1, fs2),
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Oct 20 18:13:17 2021 +0200
@@ -65,7 +65,6 @@
(
type T = (typ * term_postprocessor) list
val empty = []
- val extend = I
fun merge data = AList.merge (op =) (K true) data
)
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML Wed Oct 20 18:13:17 2021 +0200
@@ -89,7 +89,6 @@
(
type T = raw_param list
val empty = default_default_params |> map (apsnd single)
- val extend = I
fun merge data = AList.merge (op =) (K true) data
);
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Wed Oct 20 18:13:17 2021 +0200
@@ -43,7 +43,6 @@
val empty =
{types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
- val extend = I;
fun merge
({types = types1, constrs = constrs1, cases = cases1},
{types = types2, constrs = constrs2, cases = cases2}) : T =
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Oct 20 18:13:17 2021 +0200
@@ -95,7 +95,6 @@
type T = code_options
val empty = {ensure_groundness = false, limit_globally = NONE,
limited_types = [], limited_predicates = [], replacing = [], manual_reorder = []}
- val extend = I;
fun merge
({ensure_groundness = ensure_groundness1, limit_globally = limit_globally1,
limited_types = limited_types1, limited_predicates = limited_predicates1,
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Oct 20 18:13:17 2021 +0200
@@ -131,7 +131,6 @@
(
type T = pred_data Graph.T;
val empty = Graph.empty;
- val extend = I;
val merge =
Graph.join (fn key => fn (x, y) =>
if eq_pred_data (x, y)
@@ -427,7 +426,6 @@
(
type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table
val empty = Symtab.empty
- val extend = I
fun merge data : T = Symtab.merge (K true) data
);
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Oct 20 18:13:17 2021 +0200
@@ -34,7 +34,6 @@
{ignore_consts = Symtab.empty,
keep_functions = Symtab.empty,
processed_specs = Symtab.empty};
- val extend = I;
fun merge
({ignore_consts = c1, keep_functions = k1, processed_specs = s1},
{ignore_consts = c2, keep_functions = k2, processed_specs = s2}) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Oct 20 18:13:17 2021 +0200
@@ -22,7 +22,6 @@
(
type T = (term * term) Item_Net.T;
val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst);
- val extend = I;
val merge = Item_Net.merge;
)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Oct 20 18:13:17 2021 +0200
@@ -20,7 +20,6 @@
(
type T = (term * term) Item_Net.T
val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst)
- val extend = I
val merge = Item_Net.merge
)
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Oct 20 18:13:17 2021 +0200
@@ -48,7 +48,6 @@
(
type T = simpset * term list;
val empty = (HOL_ss, allowed_consts);
- val extend = I;
fun merge ((ss1, ts1), (ss2, ts2)) =
(merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
);
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Oct 20 18:13:17 2021 +0200
@@ -256,7 +256,6 @@
(
type T = (term * string) list
val empty = []
- val extend = I
fun merge data : T = AList.merge (op =) (K true) data
)
--- a/src/HOL/Tools/Quotient/quotient_info.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Wed Oct 20 18:13:17 2021 +0200
@@ -81,7 +81,6 @@
quotients Symtab.table *
quotconsts list Symtab.table
val empty: T = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty)
- val extend = I
fun merge
((quotmaps1, abs_rep1, quotients1, quotconsts1),
(quotmaps2, abs_rep2, quotients2, quotconsts2)) : T =
--- a/src/HOL/Tools/SMT/smt_builtin.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Wed Oct 20 18:13:17 2021 +0200
@@ -97,7 +97,6 @@
(typ -> (string * typ list) option) * (typ -> int -> string option)) ttab *
(term list bfun, bfunr option bfun) btab
val empty = ([], Symtab.empty)
- val extend = I
fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2))
)
--- a/src/HOL/Tools/SMT/smt_config.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML Wed Oct 20 18:13:17 2021 +0200
@@ -97,7 +97,6 @@
(
type T = data
val empty = empty_data
- val extend = I
val merge = merge_data
)
--- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Oct 20 18:13:17 2021 +0200
@@ -471,7 +471,6 @@
(
type T = extra_norm SMT_Util.dict
val empty = []
- val extend = I
fun merge data = SMT_Util.dict_merge fst data
)
--- a/src/HOL/Tools/SMT/smt_replay.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay.ML Wed Oct 20 18:13:17 2021 +0200
@@ -159,7 +159,6 @@
(
type T = simpset
val empty = basic_simpset
- val extend = I
val merge = Simplifier.merge_ss
)
in
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Wed Oct 20 18:13:17 2021 +0200
@@ -133,7 +133,6 @@
(int * (term abstracter -> term option abstracter)) list *
th_lemma_method Symtab.table
val empty = ([], Symtab.empty)
- val extend = I
fun merge ((abss1, ths1), (abss2, ths2)) = (
Ord_List.merge id_ord (abss1, abss2),
Symtab.merge (K true) (ths1, ths2))
--- a/src/HOL/Tools/SMT/smt_solver.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Oct 20 18:13:17 2021 +0200
@@ -187,7 +187,6 @@
(
type T = solver_info Symtab.table
val empty = Symtab.empty
- val extend = I
fun merge data = Symtab.merge (K true) data
)
--- a/src/HOL/Tools/SMT/smt_translate.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Oct 20 18:13:17 2021 +0200
@@ -473,7 +473,6 @@
(
type T = (Proof.context -> config) SMT_Util.dict
val empty = []
- val extend = I
fun merge data = SMT_Util.dict_merge fst data
)
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Wed Oct 20 18:13:17 2021 +0200
@@ -75,7 +75,6 @@
(
type T = (int * (term list -> string option)) list
val empty = []
- val extend = I
fun merge data = Ord_List.merge fst_int_ord data
)
--- a/src/HOL/Tools/SMT/smtlib_proof.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/smtlib_proof.ML Wed Oct 20 18:13:17 2021 +0200
@@ -194,7 +194,6 @@
(
type T = (int * type_parser) list * (int * term_parser) list
val empty : T = ([(serial (), core_type_parser)], [(serial (), core_term_parser)])
- val extend = I
fun merge ((tys1, ts1), (tys2, ts2)) =
(Ord_List.merge id_ord (tys1, tys2), Ord_List.merge id_ord (ts1, ts2))
)
--- a/src/HOL/Tools/SMT/verit_proof.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/verit_proof.ML Wed Oct 20 18:13:17 2021 +0200
@@ -119,7 +119,6 @@
(
type T = verit_strategy
val empty = empty_data
- val extend = I
val merge = merge_data
)
--- a/src/HOL/Tools/SMT/z3_interface.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Oct 20 18:13:17 2021 +0200
@@ -95,7 +95,6 @@
(
type T = (int * mk_builtins) list
val empty = []
- val extend = I
fun merge data = Ord_List.merge fst_int_ord data
)
--- a/src/HOL/Tools/SMT/z3_replay_rules.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_rules.ML Wed Oct 20 18:13:17 2021 +0200
@@ -16,7 +16,6 @@
(
type T = thm Net.net
val empty = Net.empty
- val extend = I
val merge = Net.merge Thm.eq_thm
)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Oct 20 18:13:17 2021 +0200
@@ -131,7 +131,6 @@
(
type T = ((unit -> atp_config) * stamp) Symtab.table
val empty = Symtab.empty
- val extend = I
fun merge data : T =
Symtab.merge (eq_snd (op =)) data
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Oct 20 18:13:17 2021 +0200
@@ -159,7 +159,6 @@
(
type T = raw_param list
val empty = default_default_params |> map (apsnd single)
- val extend = I
fun merge data : T = AList.merge (op =) (K true) data
)
--- a/src/HOL/Tools/Transfer/transfer.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Wed Oct 20 18:13:17 2021 +0200
@@ -94,7 +94,6 @@
relator_eq_raw = Thm.item_net,
relator_domain = Thm.item_net,
pred_data = Symtab.empty }
- val extend = I
fun merge
( { transfer_raw = t1, known_frees = k1,
compound_lhs = l1,
--- a/src/HOL/Tools/arith_data.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/arith_data.ML Wed Oct 20 18:13:17 2021 +0200
@@ -30,7 +30,6 @@
(
type T = (serial * (string * (Proof.context -> int -> tactic))) list;
val empty = [];
- val extend = I;
fun merge data : T = AList.merge (op =) (K true) data;
);
--- a/src/HOL/Tools/functor.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/functor.ML Wed Oct 20 18:13:17 2021 +0200
@@ -32,7 +32,6 @@
(
type T = entry list Symtab.table
val empty = Symtab.empty
- val extend = I
fun merge data = Symtab.merge (K true) data
);
--- a/src/HOL/Tools/inductive.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Oct 20 18:13:17 2021 +0200
@@ -214,7 +214,6 @@
(
type T = data;
val empty = make_data (empty_infos, [], empty_equations);
- val extend = I;
fun merge (Data {infos = infos1, monos = monos1, equations = equations1},
Data {infos = infos2, monos = monos2, equations = equations2}) =
make_data (Item_Net.merge (infos1, infos2),
--- a/src/HOL/Tools/inductive_set.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/inductive_set.ML Wed Oct 20 18:13:17 2021 +0200
@@ -148,7 +148,6 @@
pred_arities: (typ * (int list list option list * int list list option)) list Symtab.table};
val empty = {to_set_simps = [], to_pred_simps = [],
set_arities = Symtab.empty, pred_arities = Symtab.empty};
- val extend = I;
fun merge
({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1,
set_arities = set_arities1, pred_arities = pred_arities1},
--- a/src/HOL/Tools/lin_arith.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed Oct 20 18:13:17 2021 +0200
@@ -74,7 +74,6 @@
inj_consts: (string * typ) list,
discrete: string list};
val empty = {splits = [], inj_consts = [], discrete = []};
- val extend = I;
fun merge
({splits = splits1, inj_consts = inj_consts1, discrete = discrete1},
{splits = splits2, inj_consts = inj_consts2, discrete = discrete2}) : T =
--- a/src/HOL/Tools/record.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/record.ML Wed Oct 20 18:13:17 2021 +0200
@@ -79,7 +79,6 @@
(
type T = thm Symtab.table;
val empty = Symtab.make [tuple_iso_tuple];
- val extend = I;
fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *)
);
@@ -396,7 +395,6 @@
{selectors = Symtab.empty, updates = Symtab.empty,
simpset = HOL_basic_ss, defset = HOL_basic_ss}
Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
- val extend = I;
fun merge
({records = recs1,
sel_upd = {selectors = sels1, updates = upds1, simpset = ss1, defset = ds1},
--- a/src/HOL/Tools/reflection.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/reflection.ML Wed Oct 20 18:13:17 2021 +0200
@@ -50,7 +50,6 @@
(
type T = thm list * thm list;
val empty = ([], []);
- val extend = I;
fun merge ((ths1, rths1), (ths2, rths2)) =
(Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2));
);
--- a/src/HOL/Tools/semiring_normalizer.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Wed Oct 20 18:13:17 2021 +0200
@@ -60,7 +60,6 @@
(
type T = (thm * entry) list;
val empty = [];
- val extend = I;
fun merge data = AList.merge Thm.eq_thm (K true) data;
);
--- a/src/HOL/Tools/typedef.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/typedef.ML Wed Oct 20 18:13:17 2021 +0200
@@ -66,7 +66,6 @@
(
type T = info list Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data = Symtab.merge_list (K true) data;
);
--- a/src/HOL/Tools/value_command.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/value_command.ML Wed Oct 20 18:13:17 2021 +0200
@@ -20,7 +20,6 @@
(
type T = (Proof.context -> term -> term) Name_Space.table;
val empty = Name_Space.empty_table "evaluator";
- val extend = I;
val merge = Name_Space.merge_tables;
)
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Oct 20 18:13:17 2021 +0200
@@ -131,7 +131,6 @@
{add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
lessD = [], neqE = [], simpset = empty_ss,
number_of = NONE};
- val extend = I;
fun merge
({add_mono_thms = add_mono_thms1, mult_mono_thms = mult_mono_thms1, inj_thms = inj_thms1,
lessD = lessD1, neqE = neqE1, simpset = simpset1, number_of = number_of1},
--- a/src/Provers/classical.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Provers/classical.ML Wed Oct 20 18:13:17 2021 +0200
@@ -614,7 +614,6 @@
(
type T = claset;
val empty = empty_cs;
- val extend = I;
val merge = merge_cs;
);
--- a/src/Provers/order_tac.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Provers/order_tac.ML Wed Oct 20 18:13:17 2021 +0200
@@ -385,7 +385,6 @@
structure Data = Generic_Data(
type T = (order_context * (order_context -> thm list -> Proof.context -> int -> tactic)) list
val empty = []
- val extend = I
fun merge data = Library.merge order_data_eq data
)
--- a/src/Pure/Concurrent/thread_data_virtual.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Concurrent/thread_data_virtual.ML Wed Oct 20 18:13:17 2021 +0200
@@ -11,7 +11,6 @@
(
type T = Universal.universal Inttab.table;
val empty = Inttab.empty;
- val extend = I;
val merge = Inttab.merge (K true);
);
--- a/src/Pure/General/name_space.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/General/name_space.ML Wed Oct 20 18:13:17 2021 +0200
@@ -495,7 +495,6 @@
type T = naming;
val empty = global_naming;
fun init _ = local_naming;
- val extend = I;
val merge = #1;
end;
--- a/src/Pure/Isar/attrib.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Oct 20 18:13:17 2021 +0200
@@ -95,7 +95,6 @@
(
type T = ((Token.src -> attribute) * string) Name_Space.table;
val empty : T = Name_Space.empty_table Markup.attributeN;
- val extend = I;
fun merge data : T = Name_Space.merge_tables data;
);
@@ -383,7 +382,6 @@
(
type T = Config.value Config.T Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data = Symtab.merge (K true) data;
);
--- a/src/Pure/Isar/bundle.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/bundle.ML Wed Oct 20 18:13:17 2021 +0200
@@ -37,7 +37,6 @@
(
type T = Attrib.thms Name_Space.table * Attrib.thms option;
val empty : T = (Name_Space.empty_table Markup.bundleN, NONE);
- val extend = I;
fun merge ((tab1, target1), (tab2, target2)) =
(Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2));
);
--- a/src/Pure/Isar/calculation.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/calculation.ML Wed Oct 20 18:13:17 2021 +0200
@@ -34,7 +34,6 @@
(
type T = (thm Item_Net.T * thm Item_Net.T) * calculation option;
val empty = ((Thm.item_net_elim, Thm.item_net), NONE);
- val extend = I;
fun merge (((trans1, sym1), _), ((trans2, sym2), _)) =
((Item_Net.merge (trans1, trans2), Item_Net.merge (sym1, sym2)), NONE);
);
--- a/src/Pure/Isar/class.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/class.ML Wed Oct 20 18:13:17 2021 +0200
@@ -109,7 +109,6 @@
(
type T = class_data Graph.T
val empty = Graph.empty;
- val extend = I;
val merge = Graph.join merge_class_data;
);
--- a/src/Pure/Isar/code.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/code.ML Wed Oct 20 18:13:17 2021 +0200
@@ -401,7 +401,6 @@
(
type T = specs * (string * (data * Context.theory_id) option Synchronized.var);
val empty = (empty_specs, make_dataref (Context.the_global_context ()));
- val extend = I;
fun merge ((specs1, dataref), (specs2, _)) =
(merge_specs (specs1, specs2), dataref);
);
--- a/src/Pure/Isar/context_rules.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/context_rules.ML Wed Oct 20 18:13:17 2021 +0200
@@ -99,7 +99,6 @@
(
type T = rules;
val empty = make_rules ~1 [] empty_netpairs ([], []);
- val extend = I;
fun merge
(Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
--- a/src/Pure/Isar/experiment.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/experiment.ML Wed Oct 20 18:13:17 2021 +0200
@@ -18,7 +18,6 @@
(
type T = Symtab.set;
val empty = Symtab.empty;
- val extend = I;
val merge = Symtab.merge (K true);
);
--- a/src/Pure/Isar/generic_target.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML Wed Oct 20 18:13:17 2021 +0200
@@ -169,7 +169,6 @@
(
type T = (binding * (term * term list) -> Context.generic -> Context.generic) Inttab.table;
val empty = Inttab.empty;
- val extend = I;
val merge = Inttab.merge (K true);
);
--- a/src/Pure/Isar/local_defs.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/local_defs.ML Wed Oct 20 18:13:17 2021 +0200
@@ -180,7 +180,6 @@
(
type T = thm list;
val empty = [];
- val extend = I;
val merge = Thm.merge_thms;
);
--- a/src/Pure/Isar/locale.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/locale.ML Wed Oct 20 18:13:17 2021 +0200
@@ -178,7 +178,6 @@
(
type T = locale Name_Space.table;
val empty : T = Name_Space.empty_table Markup.localeN;
- val extend = I;
val merge = Name_Space.join_tables (K merge_locale);
);
@@ -288,7 +287,6 @@
(
type T = idents;
val empty = empty_idents;
- val extend = I;
val merge = merge_idents;
);
@@ -360,7 +358,6 @@
unique registration serial points to mixin list*)
type T = regs * mixins;
val empty: T = (Idtab.empty, Inttab.empty);
- val extend = I;
fun merge old_thys =
let
fun recursive_merge ((regs1, mixins1), (regs2, mixins2)) : T =
@@ -675,7 +672,6 @@
(
type T = thm Item_Net.T * thm Item_Net.T * thm Item_Net.T;
val empty = (Thm.item_net, Thm.item_net, Thm.item_net);
- val extend = I;
fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
(Item_Net.merge (witnesses1, witnesses2),
Item_Net.merge (intros1, intros2),
--- a/src/Pure/Isar/method.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/method.ML Wed Oct 20 18:13:17 2021 +0200
@@ -294,7 +294,6 @@
facts: thm list option};
val empty : T =
{methods = Name_Space.empty_table Markup.methodN, ml_tactic = NONE, facts = NONE};
- val extend = I;
fun merge
({methods = methods1, ml_tactic = ml_tactic1, facts = facts1},
{methods = methods2, ml_tactic = ml_tactic2, facts = facts2}) : T =
--- a/src/Pure/Isar/object_logic.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/object_logic.ML Wed Oct 20 18:13:17 2021 +0200
@@ -52,7 +52,6 @@
(
type T = data;
val empty = make_data (NONE, NONE, ([], []));
- 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"
--- a/src/Pure/Isar/outer_syntax.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Oct 20 18:13:17 2021 +0200
@@ -81,7 +81,6 @@
(
type T = command Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data : T =
data |> Symtab.join (fn name => fn (cmd1, cmd2) =>
if eq_command (cmd1, cmd2) then raise Symtab.SAME
--- a/src/Pure/Isar/spec_rules.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Isar/spec_rules.ML Wed Oct 20 18:13:17 2021 +0200
@@ -121,7 +121,6 @@
(
type T = spec_rule Item_Net.T;
val empty : T = Item_Net.init eq_spec #terms;
- val extend = I;
val merge = Item_Net.merge;
);
--- a/src/Pure/ML/ml_context.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/ML/ml_context.ML Wed Oct 20 18:13:17 2021 +0200
@@ -63,7 +63,6 @@
(
type T = (bool * antiquotation) Name_Space.table;
val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
- val extend = I;
fun merge data : T = Name_Space.merge_tables data;
);
--- a/src/Pure/ML/ml_env.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/ML/ml_env.ML Wed Oct 20 18:13:17 2021 +0200
@@ -117,7 +117,6 @@
(
type T = data;
val empty = empty_data;
- val extend = I;
val merge = merge_data;
);
--- a/src/Pure/ML/ml_thms.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/ML/ml_thms.ML Wed Oct 20 18:13:17 2021 +0200
@@ -111,7 +111,6 @@
(
type T = thm list;
val empty = [];
- val extend = I;
val merge = #1;
);
--- a/src/Pure/PIDE/resources.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/PIDE/resources.ML Wed Oct 20 18:13:17 2021 +0200
@@ -224,7 +224,6 @@
(
type T = files;
val empty = make_files (Path.current, [], []);
- val extend = I;
fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) =
let val provided' = Library.merge (op =) (provided1, provided2)
in make_files (master_dir, imports, provided') end
--- a/src/Pure/Proof/extraction.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Proof/extraction.ML Wed Oct 20 18:13:17 2021 +0200
@@ -213,7 +213,6 @@
defs = [],
expand = [],
prep = NONE};
- val extend = I;
fun merge
({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
--- a/src/Pure/Syntax/syntax.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Syntax/syntax.ML Wed Oct 20 18:13:17 2021 +0200
@@ -143,7 +143,6 @@
(
type T = operations option;
val empty = NONE;
- val extend = I;
val merge = merge_options;
);
--- a/src/Pure/Syntax/syntax_phases.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Oct 20 18:13:17 2021 +0200
@@ -875,7 +875,6 @@
((key * ((string * typ check) * stamp) list) list *
(key * ((string * term check) * stamp) list) list);
val empty = ([], []);
- val extend = I;
fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
(AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
--- a/src/Pure/Thy/document_antiquotation.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML Wed Oct 20 18:13:17 2021 +0200
@@ -100,7 +100,6 @@
val empty : T =
(Name_Space.empty_table Markup.document_antiquotationN,
Name_Space.empty_table Markup.document_antiquotation_optionN);
- val extend = I;
fun merge ((commands1, options1), (commands2, options2)) : T =
(Name_Space.merge_tables (commands1, commands2),
Name_Space.merge_tables (options1, options2));
--- a/src/Pure/Thy/document_marker.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Thy/document_marker.ML Wed Oct 20 18:13:17 2021 +0200
@@ -26,7 +26,6 @@
(
type T = (Token.src -> Proof.context -> Proof.context) Name_Space.table;
val empty : T = Name_Space.empty_table "document_marker";
- val extend = I;
val merge = Name_Space.merge_tables;
);
--- a/src/Pure/Thy/export_theory.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Thy/export_theory.ML Wed Oct 20 18:13:17 2021 +0200
@@ -22,7 +22,6 @@
(
type T = (theory -> Name_Space.T) Inttab.table;
val empty = Inttab.empty;
- val extend = I;
val merge = Inttab.merge (K true);
);
--- a/src/Pure/Thy/term_style.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Thy/term_style.ML Wed Oct 20 18:13:17 2021 +0200
@@ -19,7 +19,6 @@
(
type T = (Proof.context -> term -> term) parser Name_Space.table;
val empty : T = Name_Space.empty_table "antiquotation_style";
- val extend = I;
fun merge data : T = Name_Space.merge_tables data;
);
--- a/src/Pure/Thy/thy_header.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Thy/thy_header.ML Wed Oct 20 18:13:17 2021 +0200
@@ -96,7 +96,6 @@
(
type T = Keyword.keywords;
val empty = bootstrap_keywords;
- val extend = I;
val merge = Keyword.merge_keywords;
);
--- a/src/Pure/Thy/thy_info.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Oct 20 18:13:17 2021 +0200
@@ -44,7 +44,6 @@
(
type T = ((presentation_context -> theory -> unit) * stamp) list;
val empty = [];
- val extend = I;
fun merge data : T = Library.merge (eq_snd op =) data;
);
--- a/src/Pure/Tools/generated_files.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Tools/generated_files.ML Wed Oct 20 18:13:17 2021 +0200
@@ -72,7 +72,6 @@
(Symtab.empty,
Name_Space.empty_table Markup.file_typeN,
Name_Space.empty_table Markup.antiquotationN);
- val extend = I;
fun merge ((files1, types1, antiqs1), (files2, types2, antiqs2)) =
let
val files' =
--- a/src/Pure/Tools/named_theorems.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Tools/named_theorems.ML Wed Oct 20 18:13:17 2021 +0200
@@ -26,7 +26,6 @@
(
type T = thm Item_Net.T Symtab.table;
val empty: T = Symtab.empty;
- val extend = I;
val merge : T * T -> T = Symtab.join (K Item_Net.merge);
);
--- a/src/Pure/Tools/named_thms.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Tools/named_thms.ML Wed Oct 20 18:13:17 2021 +0200
@@ -22,7 +22,6 @@
(
type T = thm Item_Net.T;
val empty = Thm.item_net;
- val extend = I;
val merge = Item_Net.merge;
);
--- a/src/Pure/Tools/plugin.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Tools/plugin.ML Wed Oct 20 18:13:17 2021 +0200
@@ -29,7 +29,6 @@
(
type T = string list Name_Space.table;
val empty: T = Name_Space.empty_table "plugin";
- val extend = I;
val merge = Name_Space.merge_tables;
);
@@ -124,7 +123,6 @@
(
type T = data list * (interp * data list) list;
val empty : T = ([], []);
- val extend = I;
val merge_data = merge eq_data;
fun merge ((data1, interps1), (data2, interps2)) : T =
(merge_data (data1, data2), AList.join eq_interp (K merge_data) (interps1, interps2));
--- a/src/Pure/Tools/simplifier_trace.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML Wed Oct 20 18:13:17 2021 +0200
@@ -47,7 +47,6 @@
memory = true,
parent = 0,
breakpoints = empty_breakpoints}
- val extend = I
fun merge
({max_depth = max_depth1, mode = mode1, interactive = interactive1,
memory = memory1, breakpoints = breakpoints1, ...}: T,
--- a/src/Pure/axclass.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/axclass.ML Wed Oct 20 18:13:17 2021 +0200
@@ -81,7 +81,6 @@
(
type T = data;
val empty = make_data (Symtab.empty, [], (Symtab.empty, Symtab.empty));
- val extend = I;
fun merge old_thys
(Data {axclasses = axclasses1, params = params1, inst_params = inst_params1},
Data {axclasses = axclasses2, params = params2, inst_params = inst_params2}) =
--- a/src/Pure/config.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/config.ML Wed Oct 20 18:13:17 2021 +0200
@@ -136,7 +136,6 @@
(
type T = value Inttab.table;
val empty = Inttab.empty;
- val extend = I;
fun merge data = Inttab.merge (K true) data;
);
--- a/src/Pure/context.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/context.ML Wed Oct 20 18:13:17 2021 +0200
@@ -96,8 +96,7 @@
include CONTEXT
structure Theory_Data:
sig
- val declare: Position.T -> Any.T -> (Any.T -> Any.T) ->
- (theory * theory -> Any.T * Any.T -> Any.T) -> serial
+ val declare: Position.T -> Any.T -> (theory * theory -> Any.T * Any.T -> Any.T) -> serial
val get: serial -> (Any.T -> 'a) -> theory -> 'a
val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
end
@@ -266,7 +265,6 @@
type kind =
{pos: Position.T,
empty: Any.T,
- extend: Any.T -> Any.T,
merge: theory * theory -> Any.T * Any.T -> Any.T};
val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
@@ -284,18 +282,16 @@
fun invoke_pos k = invoke "" (K o #pos) k ();
fun invoke_empty k = invoke "" (K o #empty) k ();
-val invoke_extend = invoke "extend" #extend;
fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
-fun declare_theory_data pos empty extend merge =
+fun declare_theory_data pos empty merge =
let
val k = serial ();
- val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
+ val kind = {pos = pos, empty = empty, merge = merge};
val _ = Synchronized.change kinds (Datatab.update (k, kind));
in k end;
-val extend_data = Datatab.map invoke_extend;
-fun merge_data thys = Datatab.join (invoke_merge thys) o apply2 extend_data;
+fun merge_data thys = Datatab.join (invoke_merge thys);
end;
@@ -357,20 +353,20 @@
let
val ({id, ids}, {name, stage}) = rep_theory_id (theory_id thy);
val Theory (_, ancestry, data) = thy;
- val (ancestry', data') =
- if is_none stage then
- (make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)), extend_data data)
- else (ancestry, data);
+ val ancestry' =
+ if is_none stage
+ then make_ancestry [thy] (extend_ancestors thy (ancestors_of thy))
+ else ancestry;
val history' = {name = name, stage = if finish then NONE else Option.map next_stage stage};
val ids' = insert_id id ids;
- val data'' = f data';
- in create_thy ids' history' ancestry' data'' end;
+ val data' = f data;
+ in create_thy ids' history' ancestry' data' end;
in
val update_thy = change_thy false;
val extend_thy = update_thy I;
-val finish_thy = change_thy true I #> tap extend_thy;
+val finish_thy = change_thy true I;
end;
@@ -639,7 +635,6 @@
sig
type T
val empty: T
- val extend: T -> T
val merge: theory * theory -> T * T -> T
end;
@@ -647,7 +642,6 @@
sig
type T
val empty: T
- val extend: T -> T
val merge: T * T -> T
end;
@@ -670,13 +664,6 @@
Context.Theory_Data.declare
pos
(Data Data.empty)
- (fn Data x =>
- let
- val y = Data.extend x;
- val _ =
- if pointer_eq (x, y) then ()
- else raise Fail ("Theory_Data extend needs to be identity" ^ Position.here pos)
- in Data y end)
(fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2)))
end;
@@ -691,7 +678,6 @@
(
type T = Data.T;
val empty = Data.empty;
- val extend = Data.extend;
fun merge _ = Data.merge;
);
@@ -735,7 +721,6 @@
sig
type T
val empty: T
- val extend: T -> T
val merge: T * T -> T
end;
--- a/src/Pure/ex/Def.thy Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/ex/Def.thy Wed Oct 20 18:13:17 2021 +0200
@@ -36,7 +36,6 @@
(
type T = def Item_Net.T;
val empty : T = Item_Net.init eq_def (single o #lhs);
- val extend = I;
val merge = Item_Net.merge;
);
--- a/src/Pure/global_theory.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/global_theory.ML Wed Oct 20 18:13:17 2021 +0200
@@ -64,7 +64,6 @@
(
type T = Facts.T * Thm_Name.T Inttab.table lazy option;
val empty: T = (Facts.empty, NONE);
- val extend = I;
fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), NONE);
);
--- a/src/Pure/more_thm.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/more_thm.ML Wed Oct 20 18:13:17 2021 +0200
@@ -665,7 +665,6 @@
(
type T = thm list lazy Inttab.table;
val empty = Inttab.empty;
- val extend = I;
val merge = Inttab.merge (K true);
);
--- a/src/Pure/proofterm.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/proofterm.ML Wed Oct 20 18:13:17 2021 +0200
@@ -1589,7 +1589,6 @@
(theory -> proof -> proof) option;
val empty = (([], []), NONE);
- val extend = I;
fun merge (((rules1, procs1), preproc1), ((rules2, procs2), preproc2)) : T =
((AList.merge (op =) (K true) (rules1, rules2),
AList.merge (op =) (K true) (procs1, procs2)),
--- a/src/Pure/pure_thy.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/pure_thy.ML Wed Oct 20 18:13:17 2021 +0200
@@ -46,7 +46,6 @@
(
type T = bool;
val empty = false;
- val extend = I;
fun merge (b1, b2) : T =
if b1 = b2 then b1
else error "Cannot merge theories with different application syntax";
--- a/src/Pure/raw_simplifier.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/raw_simplifier.ML Wed Oct 20 18:13:17 2021 +0200
@@ -347,7 +347,6 @@
(
type T = simpset;
val empty = empty_ss;
- val extend = I;
val merge = merge_ss;
);
@@ -859,7 +858,6 @@
val empty: T =
{trace_invoke = fn _ => fn ctxt => ctxt,
trace_apply = fn _ => fn ctxt => fn cont => cont ctxt};
- val extend = I;
fun merge (trace_ops, _) = trace_ops;
);
--- a/src/Pure/sign.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/sign.ML Wed Oct 20 18:13:17 2021 +0200
@@ -134,7 +134,6 @@
structure Data = Theory_Data'
(
type T = sign;
- val extend = I;
val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
fun merge old_thys (sign1, sign2) =
let
--- a/src/Pure/simplifier.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/simplifier.ML Wed Oct 20 18:13:17 2021 +0200
@@ -101,7 +101,6 @@
(
type T = simproc Name_Space.table;
val empty : T = Name_Space.empty_table "simproc";
- val extend = I;
fun merge data : T = Name_Space.merge_tables data;
);
--- a/src/Pure/soft_type_system.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/soft_type_system.ML Wed Oct 20 18:13:17 2021 +0200
@@ -49,7 +49,6 @@
(
type T = (operations * stamp) option;
val empty = NONE;
- val extend = I;
fun merge (data as SOME (_, s), SOME (_, s')) =
if s = s' then data
else error "Cannot merge theories with different soft-type systems"
--- a/src/Pure/theory.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/theory.ML Wed Oct 20 18:13:17 2021 +0200
@@ -89,7 +89,6 @@
structure Thy = Theory_Data'
(
type T = thy;
- val extend = I;
val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], []));
fun merge old_thys (thy1, thy2) =
let
--- a/src/Pure/thm.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Pure/thm.ML Wed Oct 20 18:13:17 2021 +0200
@@ -922,7 +922,6 @@
classes; (*type classes within the logic*)
val empty : T = (Name_Space.empty_table Markup.oracleN, empty_classes);
- val extend = I;
fun merge ((oracles1, sorts1), (oracles2, sorts2)) : T =
(Name_Space.merge_tables (oracles1, oracles2), merge_classes (sorts1, sorts2));
);
--- a/src/Sequents/prover.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Sequents/prover.ML Wed Oct 20 18:13:17 2021 +0200
@@ -46,7 +46,6 @@
(
type T = pack;
val empty = empty_pack;
- val extend = I;
fun merge (Pack (safes, unsafes), Pack (safes', unsafes')) =
Pack
(sort_rules (Thm.merge_thms (safes, safes')),
--- a/src/Tools/Code/code_preproc.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Tools/Code/code_preproc.ML Wed Oct 20 18:13:17 2021 +0200
@@ -100,7 +100,6 @@
(
type T = thmproc;
val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
- val extend = I;
val merge = merge_thmproc;
);
@@ -319,7 +318,6 @@
(
type T = string list option;
val empty = SOME [];
- val extend = I;
fun merge (NONE, _) = NONE
| merge (_, NONE) = NONE
| merge (SOME cs1, SOME cs2) = SOME (Library.merge (op =) (cs1, cs2));
--- a/src/Tools/Code/code_runtime.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Tools/Code/code_runtime.ML Wed Oct 20 18:13:17 2021 +0200
@@ -340,7 +340,6 @@
(
type T = thm list;
val empty = [];
- val extend = I;
val merge = Library.merge Thm.eq_thm_prop;
);
@@ -800,7 +799,6 @@
(
type T = string list
val empty = []
- val extend = I
fun merge data : T = Library.merge (op =) data
);
--- a/src/Tools/Code/code_simp.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Tools/Code/code_simp.ML Wed Oct 20 18:13:17 2021 +0200
@@ -26,7 +26,6 @@
(
type T = simpset;
val empty = empty_ss;
- val extend = I;
val merge = merge_ss;
);
--- a/src/Tools/Code/code_target.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Tools/Code/code_target.ML Wed Oct 20 18:13:17 2021 +0200
@@ -186,7 +186,6 @@
(
type T = (target * Code_Printer.data) Symtab.table * int;
val empty = (Symtab.empty, 0);
- val extend = I;
fun merge ((targets1, index1), (targets2, index2)) : T =
let
val targets' =
--- a/src/Tools/induct.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Tools/induct.ML Wed Oct 20 18:13:17 2021 +0200
@@ -233,7 +233,6 @@
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)),
simpset_of (empty_simpset \<^context>
addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq]));
- val extend = I;
fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1),
((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) =
((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),
--- a/src/Tools/nbe.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Tools/nbe.ML Wed Oct 20 18:13:17 2021 +0200
@@ -45,7 +45,6 @@
(
type T = (class * thm) list;
val empty = [];
- val extend = I;
fun merge data : T = AList.merge (op =) (K true) data;
);
--- a/src/Tools/quickcheck.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Tools/quickcheck.ML Wed Oct 20 18:13:17 2021 +0200
@@ -213,7 +213,6 @@
(string * (Proof.context -> term list -> (int -> bool) list)) list *
test_params;
val empty = ([], [], [], Test_Params {default_type = [], expect = No_Expectation});
- val extend = I;
fun merge
((testers1, batch_generators1, batch_validators1, params1),
(testers2, batch_generators2, batch_validators2, params2)) : T =
--- a/src/Tools/subtyping.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Tools/subtyping.ML Wed Oct 20 18:13:17 2021 +0200
@@ -49,7 +49,6 @@
(
type T = data;
val empty = make_data (Symreltab.empty, Graph.empty, Graph.empty, Symtab.empty, Symtab.empty);
- val extend = I;
fun merge
(Data {coes = coes1, full_graph = full_graph1, coes_graph = coes_graph1,
tmaps = tmaps1, coerce_args = coerce_args1},
--- a/src/Tools/try.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/Tools/try.ML Wed Oct 20 18:13:17 2021 +0200
@@ -39,7 +39,6 @@
(
type T = tool list;
val empty = [];
- val extend = I;
fun merge data : T = Ord_List.merge tool_ord data;
);
--- a/src/ZF/Tools/ind_cases.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/ZF/Tools/ind_cases.ML Wed Oct 20 18:13:17 2021 +0200
@@ -20,7 +20,6 @@
(
type T = (Proof.context -> conv) Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data = Symtab.merge (K true) data;
);
--- a/src/ZF/Tools/induct_tacs.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Wed Oct 20 18:13:17 2021 +0200
@@ -34,7 +34,6 @@
(
type T = datatype_info Symtab.table;
val empty = Symtab.empty;
- val extend = I;
fun merge data : T = Symtab.merge (K true) data;
);
@@ -53,7 +52,6 @@
(
type T = constructor_info Symtab.table
val empty = Symtab.empty
- val extend = I
fun merge data = Symtab.merge (K true) data;
);
--- a/src/ZF/Tools/typechk.ML Wed Oct 20 17:11:46 2021 +0200
+++ b/src/ZF/Tools/typechk.ML Wed Oct 20 18:13:17 2021 +0200
@@ -43,7 +43,6 @@
(
type T = tcset;
val empty = TC {rules = [], net = Net.empty};
- val extend = I;
fun merge (TC {rules, net}, TC {rules = rules', net = net'}) =
TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')};
);