src/HOL/Library/bnf_lfp_countable.ML

--- a/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 22:47:05 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 22:47:05 2014 +0200
@@ -23,7 +23,7 @@
 
 fun nchotomy_tac nchotomy =
   HEADGOAL (rtac (nchotomy RS @{thm all_reg[rotated]}) THEN'
-    REPEAT_ALL_NEW (match_tac [allI, impI]) THEN' REPEAT_ALL_NEW (ematch_tac [exE, disjE]));
+    REPEAT_ALL_NEW (resolve_tac [allI, impI] ORELSE' eresolve_tac [exE, disjE]));
 
 fun meta_spec_mp_tac 0 = K all_tac
   | meta_spec_mp_tac depth =