# HG changeset patch
# User blanchet
# Date 1382028780 -7200
# Node ID e475d86ab2ca7ec6e9786548948c45d2fce783b0
# Parent  c206cb2a3afe54ebf263f25ae8f2c08a82e78b36
handle nested tuples in 'let's

diff -r c206cb2a3afe -r e475d86ab2ca src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 17 16:45:54 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Oct 17 18:53:00 2013 +0200
@@ -269,13 +269,17 @@
   end;
 
 fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1))
-  | unfold_let (Const (@{const_name prod_case}, _) $ (t as Abs (s1, T1, Abs (s2, T2, t'))) $ u) =
-    let
-      val x = (s1 ^ s2, Term.maxidx_of_term t + 1);
-      val v = Var (x, HOLogic.mk_prodT (T1, T2));
-    in
-      unfold_let (Term.subst_Vars [(x, u)] (betapplys (t, [HOLogic.mk_fst v, HOLogic.mk_snd v])))
-    end
+  | unfold_let (Const (@{const_name prod_case}, _) $ t) =
+    (case unfold_let t of
+      t' as Abs (s1, T1, Abs (s2, T2, _)) =>
+      let
+        val x = (s1 ^ s2, Term.maxidx_of_term t + 1);
+        val v = Var (x, HOLogic.mk_prodT (T1, T2));
+      in
+        lambda v (unfold_let (betapplys (t', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
+      end
+    | _ => t)
+  | unfold_let (t $ u) = betapply (unfold_let t, u)
   | unfold_let t = t;
 
 fun fold_rev_let_if_case ctxt f bound_Ts t =