# HG changeset patch
# User blanchet
# Date 1389286312 -3600
# Node ID 99eebac5fcb3e68fe15bc17b2189262ad26e1b30
# Parent  80a1931267ce2b85b25594a80c256125158024b5
fixed de Bruijn bug in 'unfold_lets'

diff -r 80a1931267ce -r 99eebac5fcb3 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- 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)