diff -r 6ec40bc934e1 -r 50a9e2fa4f6b src/Provers/clasimp.ML
--- 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;