# HG changeset patch
# User blanchet
# Date 1389615849 -3600
# Node ID 96dfb73bb11aa349dd1d02512d7f85f5e4b5bfd0
# Parent  c65fd9218ea13cfefccf48ad5a07c6fef969d93b
repaired 'ctr' tactic w.r.t. 'split'

diff -r c65fd9218ea1 -r 96dfb73bb11a src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Mon Jan 13 07:33:51 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Mon Jan 13 13:24:09 2014 +0100
@@ -143,7 +143,7 @@
 fun mk_primcorec_ctr_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 (unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl);
+  unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl);
 
 fun inst_split_eq ctxt split =
   (case prop_of split of