src/HOL/Tools/Transfer/transfer.ML

     val rules = extra_rules @ get_transfer_raw ctxt
     val eq_rules = get_relator_eq_raw ctxt
     val err_msg = "Transfer failed to convert goal to an object-logic formula"
     val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
     val thm1 = Drule.forall_intr_vars thm
-    val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
-                |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
+    val instT =
+      rev (Term.add_tvars (Thm.full_prop_of thm1) [])
+      |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
     val thm2 = thm1
-      |> Thm.certify_instantiate ctxt (instT, [])
+      |> Thm.instantiate (instT, [])
       |> Raw_Simplifier.rewrite_rule ctxt pre_simps
     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
     val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
     val rule = transfer_rule_of_lhs ctxt' t
     val tac =

         THEN_ALL_NEW
           (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
             THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
         handle TERM (_, ts) => raise TERM (err_msg, ts)
     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
-    val tnames = map (fst o dest_TFree o snd) instT
+    val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
   in
     thm3
       |> Raw_Simplifier.rewrite_rule ctxt' post_simps
       |> Simplifier.norm_hhf ctxt'
       |> Drule.generalize (tnames, [])

     val rules = extra_rules @ get_transfer_raw ctxt
     val eq_rules = get_relator_eq_raw ctxt
     val err_msg = "Transfer failed to convert goal to an object-logic formula"
     val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
     val thm1 = Drule.forall_intr_vars thm
-    val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])
-                |> map (fn v as ((a, _), S) => (v, TFree (a, S)))
+    val instT =
+      rev (Term.add_tvars (Thm.full_prop_of thm1) [])
+      |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
     val thm2 = thm1
-      |> Thm.certify_instantiate ctxt (instT, [])
+      |> Thm.instantiate (instT, [])
       |> Raw_Simplifier.rewrite_rule ctxt pre_simps
     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
     val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
     val rule = transfer_rule_of_term ctxt' true t
     val tac =

         THEN_ALL_NEW
           (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules)
             THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
         handle TERM (_, ts) => raise TERM (err_msg, ts)
     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)
-    val tnames = map (fst o dest_TFree o snd) instT
+    val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT
   in
     thm3
       |> Raw_Simplifier.rewrite_rule ctxt' post_simps
       |> Simplifier.norm_hhf ctxt'
       |> Drule.generalize (tnames, [])