diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -338,7 +338,8 @@
                  val pis'' = fold (concat_perm #> map) pis' pis;
                  val env = Pattern.first_order_match thy (ihypt, Thm.prop_of ihyp)
                    (Vartab.empty, Vartab.empty);
-                 val ihyp' = Thm.instantiate ([], map (apply2 (Thm.global_cterm_of thy))
+                 val ihyp' = Thm.instantiate ([],
+                   map (fn (v, t) => (dest_Var v, Thm.global_cterm_of thy t))
                    (map (Envir.subst_term env) vs ~~
                     map (fold_rev (NominalDatatype.mk_perm [])
                       (rev pis' @ pis)) params' @ [z])) ihyp;