# HG changeset patch # User blanchet # Date 1391614402 -3600 # Node ID 1401434a7e833d2636c81dce5ea6b892339bef8c # Parent 8192d3acadbeeac1e858fdbfc4ae5efc9c2d823a fixed handling of 'split' diff -r 8192d3acadbe -r 1401434a7e83 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 05 15:44:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 05 16:33:22 2014 +0100 @@ -63,11 +63,11 @@ (fn phi => Data.map (Typtab.default (key, morph_n2m_sugar phi n2m_sugar))); fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1)) - | unfold_let (Const (@{const_name prod_case}, _) $ t) = - (case unfold_let t of - t' as Abs (s1, T1, Abs (s2, T2, _)) => - 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]))) + | unfold_let (t as Const (@{const_name prod_case}, _) $ u) = + (case unfold_let u of + u' as Abs (s1, T1, Abs (s2, T2, _)) => + let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in + lambda v (incr_boundvars 1 (betapplys (u', [HOLogic.mk_fst v, HOLogic.mk_snd v]))) end | _ => t) | unfold_let (t $ u) = betapply (unfold_let t, unfold_let u)