# HG changeset patch
# User bulwahn
# Date 1285749194 -7200
# Node ID a8c52b982ff20e026c8e42d5c35e5d4926611a94
# Parent  2053638a2bf298299fc760fa24d07d163f43519d
putting the last step of the proof in a TRY block to handle the case that the simplifier already solved the goal

diff -r 2053638a2bf2 -r a8c52b982ff2 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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