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;