--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Thu Jan 09 17:13:05 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Thu Jan 09 17:51:52 2014 +0100
@@ -66,11 +66,8 @@
| unfold_let (Const (@{const_name prod_case}, _) $ t) =
(case unfold_let t of
t' as Abs (s1, T1, Abs (s2, T2, _)) =>
- let
- val x = (s1 ^ s2, Term.maxidx_of_term t + 1);
- val v = Var (x, HOLogic.mk_prodT (T1, T2));
- in
- lambda v (unfold_let (betapplys (t', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
+ let val v = Var ((s1 ^ s2, Term.maxidx_of_term t' + 1), HOLogic.mk_prodT (T1, T2)) in
+ lambda v (incr_boundvars 1 (betapplys (t', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
end
| _ => t)
| unfold_let (t $ u) = betapply (unfold_let t, unfold_let u)