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);
 );