diff -r b3fa4a8cdb5f -r 757549b4bbe6 src/HOL/Tools/SMT/smt_solver.ML
--- 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