diff -r f6e8293747fd -r 48dd1cefb4ae src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -146,9 +146,7 @@
 fun inst_params thy (vs, p) th cts =
   let val env = Pattern.first_order_match thy (p, Thm.prop_of th)
     (Vartab.empty, Vartab.empty)
-  in Thm.instantiate ([],
-    map (Envir.subst_term env #> Thm.global_cterm_of thy) vs ~~ cts) th
-  end;
+  in Thm.instantiate ([], map (dest_Var o Envir.subst_term env) vs ~~ cts) th end;
 
 fun prove_strong_ind s alt_name avoids ctxt =
   let