Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid REPEAT after THEN_ALL_NEW
authorhaftmann
Fri, 25 Jun 2010 11:42:29 +0200
changeset 37558 51f5dde7195d
parent 37547 a92a7f45ca28
child 37559 9118ce1d1750
avoid REPEAT after THEN_ALL_NEW
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle