src/Pure/Proof/proof_checker.ML

             val tvars = build_rev (Term.add_tvars (Thm.full_prop_of thm));
             val (fmap, thm') = Thm.varifyT_global' TFrees.empty thm;
             val ctye =
               (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
           in
-            Thm.instantiate (ctye, []) (Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
+            Thm.instantiate (TVars.make ctye, Vars.empty)
+              (Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
           end;
 
         fun thm_of _ _ (PThm ({name, prop = prop', types = SOME Ts, ...}, _)) =
               let
                 val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));