# HG changeset patch
# User blanchet
# Date 1416828913 -3600
# Node ID 2a23235632b207a3b5796aeb8afc709b6208ca6a
# Parent  ac836bcddb3b7eb2ede0086fb6184d6b14fd6ee2
careful with de Bruijn indices

diff -r ac836bcddb3b -r 2a23235632b2 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Nov 24 12:35:13 2014 +0100
@@ -310,7 +310,7 @@
           val var = Var ((Name.uu, Term.maxidx_of_term t + 1),
             domain_type (fastype_of1 (bound_Ts, t)));
         in
-          Term.lambda var (massage_call bound_Ts U T (betapply (t, var)))
+          Term.lambda var (Term.incr_boundvars 1 (massage_call bound_Ts U T (betapply (t, var))))
         end)
     and massage_call bound_Ts U T =
       massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
@@ -890,6 +890,7 @@
           else Const (@{const_name undefined}, T))
       |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
       |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss;
+
     fun currys [] t = t
       | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0))
           |> fold_rev (Term.abs o pair Name.uu) Ts;