src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 60696 8304fb4fb823
parent 59582 0fbed69ff081
child 60752 b48830b670a1
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Jul 08 19:28:43 2015 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Jul 08 21:33:00 2015 +0200
     1.3 @@ -145,20 +145,20 @@
     1.4      THEN trace_tac ctxt options "after prove_match:"
     1.5      THEN (DETERM (TRY
     1.6             (rtac eval_if_P 1
     1.7 -           THEN (SUBPROOF (fn {prems, ...} =>
     1.8 +           THEN (SUBPROOF (fn {prems, context = ctxt', ...} =>
     1.9               (REPEAT_DETERM (rtac @{thm conjI} 1
    1.10 -             THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1))))
    1.11 -             THEN trace_tac ctxt options "if condition to be solved:"
    1.12 -             THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
    1.13 +             THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1))))
    1.14 +             THEN trace_tac ctxt' options "if condition to be solved:"
    1.15 +             THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1
    1.16               THEN TRY (
    1.17                  let
    1.18                    val prems' = maps dest_conjunct_prem (take nargs prems)
    1.19                  in
    1.20 -                  rewrite_goal_tac ctxt
    1.21 +                  rewrite_goal_tac ctxt'
    1.22                      (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    1.23                  end
    1.24               THEN REPEAT_DETERM (rtac @{thm refl} 1))
    1.25 -             THEN trace_tac ctxt options "after if simp; in SUBPROOF") ctxt 1))))
    1.26 +             THEN trace_tac ctxt' options "after if simp; in SUBPROOF") ctxt 1))))
    1.27      THEN trace_tac ctxt options "after if simplification"
    1.28    end;
    1.29