# HG changeset patch
# User nipkow
# Date 1008157202 -3600
# Node ID 18ba10cc782f5979289a6ba0858ddaff4752e33b
# Parent  0404454d97df0b4dbd8568437b2d7ce078e31bf5
Removed pointless backtracking from arith_tac

diff -r 0404454d97df -r 18ba10cc782f src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Dec 12 11:07:42 2001 +0100
+++ b/src/HOL/simpdata.ML	Wed Dec 12 12:40:02 2001 +0100
@@ -336,12 +336,13 @@
       val prem_nnf_tac = full_simp_tac nnf_simpset;
 
       val refute_prems_tac =
-        REPEAT(eresolve_tac [conjE, exE] 1 ORELSE
+        REPEAT_DETERM
+              (eresolve_tac [conjE, exE] 1 ORELSE
                filter_prems_tac test 1 ORELSE
                etac disjE 1) THEN
         ((etac notE 1 THEN eq_assume_tac 1) ORELSE
          ref_tac 1);
   in EVERY'[TRY o filter_prems_tac test,
-            DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
+            REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
             SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   end;