src/HOL/Library/Old_SMT/old_smt_solver.ML
changeset 60695 757549b4bbe6
parent 59634 4b94cc030ba0
child 60752 b48830b670a1
--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -281,7 +281,7 @@
       |> Config.put Old_SMT_Config.oracle false
       |> Config.put Old_SMT_Config.filter_only_facts true
 
-    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 cnot |-> Thm.apply
     val cprop =
       (case try negate (Thm.rhs_of (Old_SMT_Normalize.atomize_conv ctxt' concl)) of