1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Jun 23 16:28:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 24 18:45:31 2010 +0200
     1.3 @@ -2520,6 +2520,8 @@
     1.4    let
     1.5      val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
     1.6      val (in_ts, clause_out_ts) = split_mode mode ts;
     1.7 +    val split_ss = HOL_basic_ss' addsimps [@{thm split_eta}, @{thm split_beta},
     1.8 +      @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
     1.9      fun prove_prems2 out_ts [] =
    1.10        print_tac options "before prove_match2 - last call:"
    1.11        THEN prove_match2 options ctxt out_ts
    1.12 @@ -2530,14 +2532,12 @@
    1.13        THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
    1.14        THEN (asm_full_simp_tac HOL_basic_ss' 1)
    1.15        THEN SOLVED (print_tac options "state before applying intro rule:"
    1.16 -      THEN (rtac pred_intro_rule 1)
    1.17 +      THEN (rtac pred_intro_rule
    1.18        (* How to handle equality correctly? *)
    1.19 -      THEN (print_tac options "state before assumption matching")
    1.20 -      THEN (REPEAT (atac 1 ORELSE 
    1.21 -         (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
    1.22 -           [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"},
    1.23 -             @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
    1.24 -          THEN print_tac options "state after simp_tac:"))))
    1.25 +      THEN_ALL_NEW (K (print_tac options "state before assumption matching")
    1.26 +      THEN' (fn i => REPEAT (atac i ORELSE (CHANGED (asm_full_simp_tac split_ss i)
    1.27 +        THEN print_tac options "state after pre-simplification:")))
    1.28 +      THEN' (K (print_tac options "state after assumption matching:")))) 1)
    1.29      | prove_prems2 out_ts ((p, deriv) :: ps) =
    1.30        let
    1.31          val mode = head_mode_of deriv