improved unfolding of 'let's

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Aug 12 15:48:59 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Aug 12 15:48:59 2014 +0200
@@ -62,18 +62,19 @@
     (fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar)));
 
 fun unfold_lets_splits (Const (@{const_name Let}, _) $ t $ u) =
-    unfold_lets_splits (betapply (u, unfold_splits_lets t))
+    unfold_lets_splits (betapply (unfold_splits_lets u, t))
   | unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u)
   | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
   | unfold_lets_splits t = t
-and unfold_splits_lets (t as Const (@{const_name case_prod}, _) $ u) =
+and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ u) =
     (case unfold_splits_lets 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_splits_lets (t $ u) = betapply (unfold_lets_splits t, u)
+    | _ => t $ unfold_lets_splits u)
+  | unfold_splits_lets (t as Const (@{const_name Let}, _) $ _ $ _) = unfold_lets_splits t
+  | unfold_splits_lets (t $ u) = betapply (unfold_splits_lets t, unfold_lets_splits u)
   | unfold_splits_lets (Abs (s, T, t)) = Abs (s, T, unfold_splits_lets t)
   | unfold_splits_lets t = unfold_lets_splits t;