# HG changeset patch
# User blanchet
# Date 1389276504 -3600
# Node ID a2f4cf3387fc0920f13d5679fcb5bea8513d4c40
# Parent  d9fd054a33864ebe3f3a6bac5789d7e32922a728
strengthen tac w.r.t. lets with tuples

diff -r d9fd054a3386 -r a2f4cf3387fc src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 09 15:08:05 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 09 15:08:24 2014 +0100
@@ -36,6 +36,7 @@
 val split_if = @{thm split_if};
 val split_if_asm = @{thm split_if_asm};
 val split_connectI = @{thms allI impI conjI};
+val unfold_lets = @{thms Let_def[abs_def] split_beta}
 
 fun exhaust_inst_as_projs ctxt frees thm =
   let
@@ -133,7 +134,7 @@
 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc_fun_opt sel_funs =
   HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
     (the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN
-  unfold_thms_tac ctxt (Let_def :: sel_funs) THEN HEADGOAL (rtac refl);
+  unfold_thms_tac ctxt (unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl);
 
 fun inst_split_eq ctxt split =
   (case prop_of split of