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},