# HG changeset patch
# User blanchet
# Date 1388697780 -3600
# Node ID 7fad0747e40f059412f19b5a8bd97c056146e19d
# Parent  790362e13e0d8a106d7e26449d387f0efc8c9ae8
made tactic behave better w.r.t. HO unification (might not be enough, and might have to fix some variables eventually though...)

diff -r 790362e13e0d -r 7fad0747e40f src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- 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;