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