# HG changeset patch
# User blanchet
# Date 1381182293 -7200
# Node ID 890f5083067baea3e7e40bb778f10252ea4a00dc
# Parent  43cdae9524bfc6bfa061ce737cf697ac559202ec
strengthened constructor-view tactic to deal with 'let's

diff -r 43cdae9524bf -r 890f5083067b src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Mon Oct 07 23:38:57 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Mon Oct 07 23:44:53 2013 +0200
@@ -85,7 +85,7 @@
 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
   HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'
     (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
-  unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
+  unfold_thms_tac ctxt (@{thm Let_def} :: sel_fs) THEN HEADGOAL (rtac refl);
 
 (* TODO: reduce code duplication with selector tactic above *)
 fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =