src/HOL/Tools/cnf.ML
changeset 60696 8304fb4fb823
parent 59642 929984c529d3
child 60759 36d9f215c982
     1.1 --- a/src/HOL/Tools/cnf.ML	Wed Jul 08 19:28:43 2015 +0200
     1.2 +++ b/src/HOL/Tools/cnf.ML	Wed Jul 08 21:33:00 2015 +0200
     1.3 @@ -539,9 +539,9 @@
     1.4  
     1.5  fun cnf_rewrite_tac ctxt i =
     1.6    (* cut the CNF formulas as new premises *)
     1.7 -  Subgoal.FOCUS (fn {prems, ...} =>
     1.8 +  Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
     1.9      let
    1.10 -      val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
    1.11 +      val cnf_thms = map (make_cnf_thm ctxt' o HOLogic.dest_Trueprop o Thm.prop_of) prems
    1.12        val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
    1.13      in
    1.14        cut_facts_tac cut_thms 1
    1.15 @@ -561,9 +561,9 @@
    1.16  
    1.17  fun cnfx_rewrite_tac ctxt i =
    1.18    (* cut the CNF formulas as new premises *)
    1.19 -  Subgoal.FOCUS (fn {prems, ...} =>
    1.20 +  Subgoal.FOCUS (fn {prems, context = ctxt', ...} =>
    1.21      let
    1.22 -      val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
    1.23 +      val cnfx_thms = map (make_cnfx_thm ctxt' o HOLogic.dest_Trueprop o Thm.prop_of) prems
    1.24        val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
    1.25      in
    1.26        cut_facts_tac cut_thms 1