src/Provers/clasimp.ML
changeset 37720 50a9e2fa4f6b
parent 36960 01594f816e3a
child 42373 fb539d6d1ac2
--- a/src/Provers/clasimp.ML	Fri Jul 02 10:47:50 2010 +0200
+++ b/src/Provers/clasimp.ML	Mon Jul 05 14:21:30 2010 +0100
@@ -203,7 +203,7 @@
           (CHANGED o nodup_depth_tac cs' n); (* slower but more general *)
     in  EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss),
                TRY (Classical.safe_tac cs),
-               REPEAT (FIRSTGOAL maintac),
+               REPEAT_DETERM (FIRSTGOAL maintac),
                TRY (Classical.safe_tac (cs addSss ss)),
                prune_params_tac]
     end;