generalized tactic to the case of several assumptions per equation

--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 22:23:00 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 23:07:49 2014 +0100
@@ -40,8 +40,9 @@
       cut_tac nchotomy THEN'
       EVERY' (map (fn k =>
           (if k < n then etac disjE else K all_tac) THEN'
-          REPEAT o (dtac meta_mp THEN' atac THEN' atac ORELSE'
-            etac conjE THEN' dtac meta_mp THEN' atac))
+          REPEAT o (dtac meta_mp THEN' atac ORELSE'
+            etac conjE THEN' dtac meta_mp THEN' atac ORELSE'
+            atac))
         ks))
   end;