diff -r 495bede1c4d9 -r 4f590c08fd5d src/HOL/Tools/legacy_transfer.ML
--- a/src/HOL/Tools/legacy_transfer.ML	Sun Jul 26 12:24:16 2015 +0200
+++ b/src/HOL/Tools/legacy_transfer.ML	Sun Jul 26 17:24:54 2015 +0200
@@ -130,7 +130,7 @@
       put_simpset HOL_ss ctxt5 addsimps (inj @ embed @ return)
       |> fold Simplifier.add_cong cong;
     val thm' = thm
-      |> Drule.cterm_instantiate (c_vars ~~ c_exprs')
+      |> infer_instantiate ctxt5 (map (#1 o dest_Var o Thm.term_of) c_vars ~~ c_exprs')
       |> fold_rev Thm.implies_intr (map Thm.cprop_of hyps)
       |> Simplifier.asm_full_simplify simpset
   in singleton (Variable.export ctxt5 ctxt1) thm' end;