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