diff -r 659117cc2963 -r 12cd198f07af src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Sun Jul 26 20:54:02 2015 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Sun Jul 26 20:56:44 2015 +0200
@@ -54,9 +54,9 @@
       end;
      val substs =
        map2 subst insts concls |> flat |> distinct (op =)
-       |> map (apply2 (Thm.cterm_of ctxt));
+       |> map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of ctxt u));
   in 
-    (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
+    (((cases, nconcls), consumes), infer_instantiate ctxt substs joined_rule) 
   end;
 
 fun rename_params_rule internal xs rule =