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 =