src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 37558 51f5dde7195d
parent 37544 456dd03e8cce
child 37591 d3daea901123
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jun 25 07:19:21 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jun 25 11:42:29 2010 +0200
     1.3 @@ -2535,8 +2535,8 @@
     1.4        THEN (rtac pred_intro_rule
     1.5        (* How to handle equality correctly? *)
     1.6        THEN_ALL_NEW (K (print_tac options "state before assumption matching")
     1.7 -      THEN' (fn i => REPEAT (atac i ORELSE (CHANGED (asm_full_simp_tac split_ss i)
     1.8 -        THEN print_tac options "state after pre-simplification:")))
     1.9 +      THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_ss) THEN' (TRY o atac)))
    1.10 +        THEN' (K (print_tac options "state after pre-simplification:"))
    1.11        THEN' (K (print_tac options "state after assumption matching:")))) 1)
    1.12      | prove_prems2 out_ts ((p, deriv) :: ps) =
    1.13        let