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
```