--- 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;