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