--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 29 10:05:44 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 29 10:33:14 2010 +0200
@@ -2556,15 +2556,17 @@
THEN (etac @{thm singleE} 1)
THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
THEN (asm_full_simp_tac HOL_basic_ss' 1)
- THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
- THEN (asm_full_simp_tac HOL_basic_ss' 1)
- THEN SOLVED (print_tac options "state before applying intro rule:"
- THEN (rtac pred_intro_rule
- (* How to handle equality correctly? *)
- THEN_ALL_NEW (K (print_tac options "state before assumption matching")
- 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)
+ THEN TRY (
+ (REPEAT_DETERM (etac @{thm Pair_inject} 1))
+ THEN (asm_full_simp_tac HOL_basic_ss' 1)
+
+ THEN SOLVED (print_tac options "state before applying intro rule:"
+ THEN (rtac pred_intro_rule
+ (* How to handle equality correctly? *)
+ THEN_ALL_NEW (K (print_tac options "state before assumption matching")
+ 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
val mode = head_mode_of deriv