changeset 74200 | 17090e27aae9 |
parent 72458 | b44e894796d5 |
child 74266 | 612b7e0d6721 |
--- a/src/HOL/Tools/SMT/smt_replay_methods.ML Wed Aug 25 22:17:38 2021 +0200 +++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Aug 26 14:45:19 2021 +0200 @@ -171,7 +171,7 @@ fun by_tac ctxt thms ns ts t tac = Goal.prove ctxt [] (map as_prop ts) (as_prop t) (fn {context, prems} => HEADGOAL (tac context prems)) - |> Drule.generalize ([], ns) + |> Drule.generalize (Symtab.empty, Symtab.make_set ns) |> discharge 1 thms fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)