src/Pure/Isar/obtain.ML

               if TVars.defined instT v then instT
               else TVars.add (v, Thm.ctyp_of ctxt (norm_type T)) instT
           | _ => 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' =
       map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
       (map snd vars @ replicate (length ys) NoSyn);