Removed pointless backtracking from arith_tac
authornipkow
Wed Dec 12 12:40:02 2001 +0100 (2001-12-12)
changeset 1247518ba10cc782f
parent 12474 0404454d97df
child 12476 eca43a50e4a4
Removed pointless backtracking from arith_tac
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Wed Dec 12 11:07:42 2001 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Dec 12 12:40:02 2001 +0100
     1.3 @@ -336,12 +336,13 @@
     1.4        val prem_nnf_tac = full_simp_tac nnf_simpset;
     1.5  
     1.6        val refute_prems_tac =
     1.7 -        REPEAT(eresolve_tac [conjE, exE] 1 ORELSE
     1.8 +        REPEAT_DETERM
     1.9 +              (eresolve_tac [conjE, exE] 1 ORELSE
    1.10                 filter_prems_tac test 1 ORELSE
    1.11                 etac disjE 1) THEN
    1.12          ((etac notE 1 THEN eq_assume_tac 1) ORELSE
    1.13           ref_tac 1);
    1.14    in EVERY'[TRY o filter_prems_tac test,
    1.15 -            DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
    1.16 +            REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
    1.17              SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
    1.18    end;