# HG changeset patch
# User blanchet
# Date 1348404773 -7200
# Node ID be6cbf960aa730cf56e9cf23b394ad9d8f51ed01
# Parent  c90818b635994df85aee51c6d98bb56e3712578e
fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)

diff -r c90818b63599 -r be6cbf960aa7 src/HOL/BNF/BNF_FP.thy
--- a/src/HOL/BNF/BNF_FP.thy	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/BNF_FP.thy	Sun Sep 23 14:52:53 2012 +0200
@@ -14,9 +14,12 @@
   "defaults"
 begin
 
-lemma case_unit: "(case u of () => f) = f"
+lemma unit_case_Unity: "(case u of () => f) = f"
 by (cases u) (hypsubst, rule unit.cases)
 
+lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
+by simp
+
 lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
 by simp
 
diff -r c90818b63599 -r be6cbf960aa7 src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
@@ -71,8 +71,8 @@
   unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
 
 val rec_like_unfold_thms =
-  @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
-      split_conv};
+  @{thms comp_def convol_def id_apply map_pair_def prod_case_Pair_iden sum.simps(5,6) sum_map.simps
+      split_conv unit_case_Unity};
 
 fun mk_rec_like_tac pre_map_defs map_ids rec_like_defs ctor_rec_like ctr_def ctxt =
   unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_ids @