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