strengthen the tactics to bring them in sync with the simplifications taking place in the code (and weaken the simplifications a bit -- let's not deal with implies)

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Sun Oct 06 20:24:06 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Sun Oct 06 20:54:28 2013 +0200
@@ -39,7 +39,7 @@
 
 fun mk_primcorec_assumption_tac ctxt discIs =
   SELECT_GOAL (unfold_thms_tac ctxt
-      @{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN
+      @{thms not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
     SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
     resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
     dresolve_tac discIs THEN' atac ORELSE'
@@ -50,14 +50,14 @@
   HEADGOAL (if m = 0 then rtac TrueI
     else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac);
 
-fun mk_primcorec_different_case_tac ctxt excl =
-  unfold_thms_tac ctxt @{thms not_not not_False_eq_True not_True_eq_False} THEN
-  HEADGOAL (rtac excl THEN_ALL_NEW mk_primcorec_assumption_tac ctxt []);
+fun mk_primcorec_different_case_tac ctxt m excl =
+  HEADGOAL (if m = 0 then mk_primcorec_assumption_tac ctxt []
+    else dtac excl THEN' (REPEAT_DETERM_N (m - 1) o atac) THEN' mk_primcorec_assumption_tac ctxt []);
 
 fun mk_primcorec_cases_tac ctxt k m exclsss =
   let val n = length exclsss in
     EVERY (map (fn [] => if k = n then all_tac else mk_primcorec_same_case_tac m
-        | [excl] => mk_primcorec_different_case_tac ctxt excl)
+        | [excl] => mk_primcorec_different_case_tac ctxt m excl)
       (take k (nth exclsss (k - 1))))
   end;
 

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Oct 06 20:24:06 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Oct 06 20:54:28 2013 +0200
@@ -157,7 +157,6 @@
   | s_not (@{const Not} $ t) = t
   | s_not (@{const conj} $ t $ u) = @{const disj} $ s_not t $ s_not u
   | s_not (@{const disj} $ t $ u) = @{const conj} $ s_not t $ s_not u
-  | s_not (@{const implies} $ t $ u) = @{const conj} $ t $ s_not u
   | s_not t = @{const Not} $ t;
 
 val s_not_conj = conjuncts_s o s_not o mk_conjs;