# 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;
 );
 \<close>
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')};
 );