# HG changeset patch
# User haftmann
# Date 1277406212 -7200
# Node ID f5a4b7ac635f174f842cd66d8dbcbba49c67d163
# Parent  2e733b0a963ce59478294fb740ce07dfd61433ff# Parent  456dd03e8ccef13a9d7ff9a091b03ae7901b39ba
merged

diff -r 2e733b0a963c -r f5a4b7ac635f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 24 18:22:15 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 24 21:03:32 2010 +0200
@@ -2520,6 +2520,8 @@
   let
     val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
     val (in_ts, clause_out_ts) = split_mode mode ts;
+    val split_ss = HOL_basic_ss' addsimps [@{thm split_eta}, @{thm split_beta},
+      @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
     fun prove_prems2 out_ts [] =
       print_tac options "before prove_match2 - last call:"
       THEN prove_match2 options ctxt out_ts
@@ -2530,14 +2532,12 @@
       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 1)
+      THEN (rtac pred_intro_rule
       (* How to handle equality correctly? *)
-      THEN (print_tac options "state before assumption matching")
-      THEN (REPEAT (atac 1 ORELSE 
-         (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
-           [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"},
-             @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
-          THEN print_tac options "state after simp_tac:"))))
+      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' (K (print_tac options "state after assumption matching:")))) 1)
     | prove_prems2 out_ts ((p, deriv) :: ps) =
       let
         val mode = head_mode_of deriv