1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 17 11:27:53 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 17 13:37:13 2013 +0200
     1.3 @@ -268,13 +268,23 @@
     1.4      massage_call
     1.5    end;
     1.6  
     1.7 +fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1))
     1.8 +  | unfold_let (Const (@{const_name prod_case}, _) $ (t as Abs (s1, T1, Abs (s2, T2, t'))) $ u) =
     1.9 +    let
    1.10 +      val x = (s1 ^ s2, Term.maxidx_of_term t + 1);
    1.11 +      val v = Var (x, HOLogic.mk_prodT (T1, T2));
    1.12 +    in
    1.13 +      unfold_let (Term.subst_Vars [(x, u)] (betapplys (t, [HOLogic.mk_fst v, HOLogic.mk_snd v])))
    1.14 +    end
    1.15 +  | unfold_let t = t;
    1.16 +
    1.17  fun fold_rev_let_if_case ctxt f bound_Ts t =
    1.18    let
    1.19      val thy = Proof_Context.theory_of ctxt;
    1.20  
    1.21      fun fld conds t =
    1.22        (case Term.strip_comb t of
    1.23 -        (Const (@{const_name Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1))
    1.24 +        (Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_let t)
    1.25        | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
    1.26          fld (conds @ conjuncts_s cond) then_branch
    1.27          o fld (conds @ s_not_conj [cond]) else_branch
    1.28 @@ -297,9 +307,6 @@
    1.29      fld [] t o pair []
    1.30    end;
    1.31  
    1.32 -fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1))
    1.33 -  | unfold_let t = t;
    1.34 -
    1.35  fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
    1.36  
    1.37  fun massage_let_if_case ctxt has_call massage_leaf =
    1.38 @@ -317,8 +324,7 @@
    1.39      and massage_rec bound_Ts t =
    1.40        let val typof = curry fastype_of1 bound_Ts in
    1.41          (case Term.strip_comb t of
    1.42 -          (Const (@{const_name Let}, _), [arg1, arg2]) =>
    1.43 -          massage_rec bound_Ts (betapply (arg2, arg1))
    1.44 +          (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_let t)
    1.45          | (Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
    1.46            let val branches' = map (massage_rec bound_Ts) branches in
    1.47              Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')