src/HOL/Tools/SMT/smt_replay_methods.ML
changeset 74561 8e6c973003c8
parent 74382 8d0294d877bd
child 78177 ea7a3cc64df5
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML	Wed Oct 20 17:11:46 2021 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML	Wed Oct 20 18:13:17 2021 +0200
@@ -133,7 +133,6 @@
     (int * (term abstracter -> term option abstracter)) list *
     th_lemma_method Symtab.table
   val empty = ([], Symtab.empty)
-  val extend = I
   fun merge ((abss1, ths1), (abss2, ths2)) = (
     Ord_List.merge id_ord (abss1, abss2),
     Symtab.merge (K true) (ths1, ths2))