# HG changeset patch
# User webertj
# Date 1180767029 -7200
# Node ID 42004f6d908bac7e22a93dcfe16e8e142de6c19b
# Parent  174b5f2ec7c1593dccdd7cd3e6ebc9540dab7d91
refute_tac made more deterministic

diff -r 174b5f2ec7c1 -r 42004f6d908b src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Sat Jun 02 03:17:44 2007 +0200
+++ b/src/HOL/simpdata.ML	Sat Jun 02 08:50:29 2007 +0200
@@ -304,7 +304,7 @@
               (eresolve_tac [@{thm conjE}, @{thm exE}] 1 ORELSE
                filter_prems_tac test 1 ORELSE
                etac @{thm disjE} 1) THEN
-        ((etac @{thm notE} 1 THEN eq_assume_tac 1) ORELSE
+        (DETERM (etac @{thm notE} 1 THEN eq_assume_tac 1) ORELSE
          ref_tac 1);
   in EVERY'[TRY o filter_prems_tac test,
             REPEAT_DETERM o etac @{thm rev_mp}, prep_tac, rtac @{thm ccontr}, prem_nnf_tac,