src/HOL/Tools/SMT/smt_solver.ML
changeset 60696 8304fb4fb823
parent 60695 757549b4bbe6
child 60752 b48830b670a1
     1.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Jul 08 19:28:43 2015 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Jul 08 21:33:00 2015 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4    fun tac prove ctxt rules =
     1.5      CONVERSION (SMT_Normalize.atomize_conv ctxt)
     1.6      THEN' rtac @{thm ccontr}
     1.7 -    THEN' SUBPROOF (fn {context = ctxt, prems, ...} => resolve (prove ctxt (rules @ prems))) ctxt
     1.8 +    THEN' SUBPROOF (fn {context = ctxt', prems, ...} => resolve (prove ctxt' (rules @ prems))) ctxt
     1.9  in
    1.10  
    1.11  val smt_tac = tac safe_solve