# HG changeset patch # User wenzelm # Date 1634746397 -7200 # Node ID 8e6c973003c8e1a29663b3e2cb20ba74af4bba69 # Parent 5c8177fd1295757556a29f00902912ec7009b8c3 discontinued obsolete "val extend = I" for data slots; diff -r 5c8177fd1295 -r 8e6c973003c8 NEWS --- 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 *** diff -r 5c8177fd1295 -r 8e6c973003c8 src/Doc/Implementation/Prelim.thy --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Algebra/ringsimp.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Analysis/measurable.ML --- 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), diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Decision_Procs/Commutative_Ring.thy --- 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); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Decision_Procs/Reflective_Field.thy --- 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); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Decision_Procs/ferrante_rackoff_data.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Decision_Procs/langford_data.ML --- 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)); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Eisbach/Tests.thy --- 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; ); \ diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Eisbach/method_closure.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/HOL.thy --- 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 ())); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/HOLCF/Tools/fixrec.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Hoare/hoare_syntax.ML --- 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" diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Import/import_data.ML --- 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 = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Library/adhoc_overloading.ML --- 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}, diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Library/code_lazy.ML --- 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 = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Library/code_test.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Library/datatype_records.ML --- 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) = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Library/old_recdef.ML --- 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 = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Library/refute.ML --- 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 = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Nominal/nominal_atoms.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Nominal/nominal_datatype.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Nominal/nominal_thmdecls.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Nonstandard_Analysis/transfer_principle.ML --- 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}, diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Real_Asymp/exp_log_expression.ML --- 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 = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Real_Asymp/multiseries_expansion.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/SPARK/Tools/spark_vcs.ML --- 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), diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Statespace/state_fun.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Statespace/state_space.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML --- 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 diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Argo/argo_tactic.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/BNF/bnf_def.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/BNF/bnf_gfp_grec.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML --- 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)); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Ctr_Sugar/case_translation.ML --- 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}) = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Function/function_common.ML --- 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 = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Function/function_context_tree.ML --- 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 ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Function/partial_function.ML --- 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; ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Function/scnp_reconstruct.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Lifting/lifting_def.ML --- 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 ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- 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 ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Lifting/lifting_info.ML --- 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 }, diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Nitpick/nitpick_commands.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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), diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Nunchaku/nunchaku_commands.ML --- 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 ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Old_Datatype/old_datatype_data.ML --- 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 = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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, diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Predicate_Compile/core_data.ML --- 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 ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- 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}) = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- 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; ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Qelim/cooper.ML --- 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)); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Quotient/quotient_info.ML --- 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 = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/smt_builtin.ML --- 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)) ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/smt_config.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/smt_normalize.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/smt_replay.ML --- 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 diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/smt_replay_methods.ML --- 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)) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/smt_solver.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/smt_translate.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/smtlib_interface.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/smtlib_proof.ML --- 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)) ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/verit_proof.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/z3_interface.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/SMT/z3_replay_rules.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- 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) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/Transfer/transfer.ML --- 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, diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/arith_data.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/functor.ML --- 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 ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/inductive.ML --- 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), diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/inductive_set.ML --- 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}, diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/lin_arith.ML --- 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 = diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/record.ML --- 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}, diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/reflection.ML --- 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)); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/semiring_normalizer.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/typedef.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/HOL/Tools/value_command.ML --- 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; ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/Provers/Arith/fast_lin_arith.ML --- 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}, diff -r 5c8177fd1295 -r 8e6c973003c8 src/Provers/classical.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Provers/order_tac.ML --- 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 ) diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Concurrent/thread_data_virtual.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/General/name_space.ML --- 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; diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/attrib.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/bundle.ML --- 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)); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/calculation.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/class.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/code.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/context_rules.ML --- 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'), ...}) = diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/experiment.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/generic_target.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/local_defs.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/locale.ML --- 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), diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/method.ML --- 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 = diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/object_logic.ML --- 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" diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/outer_syntax.ML --- 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 diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Isar/spec_rules.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/ML/ml_context.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/ML/ml_env.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/ML/ml_thms.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/PIDE/resources.ML --- 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 diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Proof/extraction.ML --- 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, diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Syntax/syntax.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Syntax/syntax_phases.ML --- 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)); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Thy/document_antiquotation.ML --- 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)); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Thy/document_marker.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Thy/export_theory.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Thy/term_style.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Thy/thy_header.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Thy/thy_info.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Tools/generated_files.ML --- 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' = diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Tools/named_theorems.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Tools/named_thms.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Tools/plugin.ML --- 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)); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/Tools/simplifier_trace.ML --- 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, diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/axclass.ML --- 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}) = diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/config.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/context.ML --- 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; diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/ex/Def.thy --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/global_theory.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/more_thm.ML --- 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); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/proofterm.ML --- 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)), diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/pure_thy.ML --- 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"; diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/raw_simplifier.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/sign.ML --- 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 diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/simplifier.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/soft_type_system.ML --- 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" diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/theory.ML --- 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 diff -r 5c8177fd1295 -r 8e6c973003c8 src/Pure/thm.ML --- 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)); ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Sequents/prover.ML --- 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')), diff -r 5c8177fd1295 -r 8e6c973003c8 src/Tools/Code/code_preproc.ML --- 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)); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Tools/Code/code_runtime.ML --- 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 ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Tools/Code/code_simp.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Tools/Code/code_target.ML --- 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' = diff -r 5c8177fd1295 -r 8e6c973003c8 src/Tools/induct.ML --- 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)), diff -r 5c8177fd1295 -r 8e6c973003c8 src/Tools/nbe.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/Tools/quickcheck.ML --- 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 = diff -r 5c8177fd1295 -r 8e6c973003c8 src/Tools/subtyping.ML --- 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}, diff -r 5c8177fd1295 -r 8e6c973003c8 src/Tools/try.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/ZF/Tools/ind_cases.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/ZF/Tools/induct_tacs.ML --- 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; ); diff -r 5c8177fd1295 -r 8e6c973003c8 src/ZF/Tools/typechk.ML --- 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')}; );