changeset 74282 | c2ee8d993d6a |
parent 74269 | f084d599bb44 |
child 74365 | b49bd5d9041f |
--- a/src/Pure/Isar/obtain.ML Thu Sep 09 23:07:02 2021 +0200 +++ b/src/Pure/Isar/obtain.ML Fri Sep 10 14:59:19 2021 +0200 @@ -335,7 +335,7 @@ | _ => instT)))); val closed_rule = rule |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var)) - |> Thm.instantiate (TVars.dest instT, []); + |> Thm.instantiate (instT, Vars.empty); val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt; val vars' =