--- a/src/HOL/Tools/SMT/smt_solver.ML Wed Jul 08 15:37:32 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Jul 08 19:28:43 2015 +0200
@@ -252,7 +252,7 @@
let
val ctxt = ctxt0 |> Config.put SMT_Config.timeout (Time.toReal time_limit)
- val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i goal
+ val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i NONE goal
fun negate ct = Thm.dest_comb ct ||> Thm.apply @{cterm Not} |-> Thm.apply
val cprop =
(case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt concl)) of