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