--- 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;