1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 17 16:45:54 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 17 18:53:00 2013 +0200
     1.3 @@ -269,13 +269,17 @@
     1.4    end;
     1.5  
     1.6  fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1))
     1.7 -  | unfold_let (Const (@{const_name prod_case}, _) $ (t as Abs (s1, T1, Abs (s2, T2, t'))) $ u) =
     1.8 -    let
     1.9 -      val x = (s1 ^ s2, Term.maxidx_of_term t + 1);
    1.10 -      val v = Var (x, HOLogic.mk_prodT (T1, T2));
    1.11 -    in
    1.12 -      unfold_let (Term.subst_Vars [(x, u)] (betapplys (t, [HOLogic.mk_fst v, HOLogic.mk_snd v])))
    1.13 -    end
    1.14 +  | unfold_let (Const (@{const_name prod_case}, _) $ t) =
    1.15 +    (case unfold_let t of
    1.16 +      t' as Abs (s1, T1, Abs (s2, T2, _)) =>
    1.17 +      let
    1.18 +        val x = (s1 ^ s2, Term.maxidx_of_term t + 1);
    1.19 +        val v = Var (x, HOLogic.mk_prodT (T1, T2));
    1.20 +      in
    1.21 +        lambda v (unfold_let (betapplys (t', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
    1.22 +      end
    1.23 +    | _ => t)
    1.24 +  | unfold_let (t $ u) = betapply (unfold_let t, u)
    1.25    | unfold_let t = t;
    1.26  
    1.27  fun fold_rev_let_if_case ctxt f bound_Ts t =