made tactic behave better w.r.t. HO unification (might not be enough, and might have to fix some variables eventually though...)

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