src/HOL/Library/refute.ML
changeset 74561 8e6c973003c8
parent 74509 f24ade4ff3cc
child 77896 a9626bcb0c3b
--- a/src/HOL/Library/refute.ML	Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Library/refute.ML	Wed Oct 20 18:13:17 2021 +0200
@@ -192,7 +192,6 @@
       (int -> bool) -> term option)) list,
      parameters: string Symtab.table};
   val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
-  val extend = I;
   fun merge
     ({interpreters = in1, printers = pr1, parameters = pa1},
      {interpreters = in2, printers = pr2, parameters = pa2}) : T =