# HG changeset patch
# User haftmann
# Date 1277458949 -7200
# Node ID 51f5dde7195dd6b1a215cbd2a989d4fb4b99ff41
# Parent  a92a7f45ca28a3e7567affda0e64f4d66dea0761
avoid REPEAT after THEN_ALL_NEW

diff -r a92a7f45ca28 -r 51f5dde7195d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jun 25 07:19:21 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jun 25 11:42:29 2010 +0200
@@ -2535,8 +2535,8 @@
       THEN (rtac pred_intro_rule
       (* How to handle equality correctly? *)
       THEN_ALL_NEW (K (print_tac options "state before assumption matching")
-      THEN' (fn i => REPEAT (atac i ORELSE (CHANGED (asm_full_simp_tac split_ss i)
-        THEN print_tac options "state after pre-simplification:")))
+      THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_ss) THEN' (TRY o atac)))
+        THEN' (K (print_tac options "state after pre-simplification:"))
       THEN' (K (print_tac options "state after assumption matching:")))) 1)
     | prove_prems2 out_ts ((p, deriv) :: ps) =
       let