# HG changeset patch
# User haftmann
# Date 1277485924 -7200
# Node ID 9118ce1d1750d5b1f9d087198b60257c3348b359
# Parent  6c7399bc0d10577829e8b4a5144530b3ddf8541c# Parent  51f5dde7195dd6b1a215cbd2a989d4fb4b99ff41
merged

diff -r 6c7399bc0d10 -r 9118ce1d1750 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jun 25 14:05:49 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jun 25 19:12:04 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