repaired 'ctr' tactic w.r.t. 'split'

--- 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