# HG changeset patch
# User boehmes
# Date 1288890115 -3600
# Node ID 82ebdd19c4a44e80e48149cbd0c505c41c734e17
# Parent  3157408633ee8749c30f4d1cc52beab0216edc6f
simulate more closely the behaviour of the tactic

diff -r 3157408633ee -r 82ebdd19c4a4 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Nov 04 17:17:21 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Nov 04 18:01:55 2010 +0100
@@ -437,15 +437,16 @@
       |> Config.put oracle false
       |> Config.put filter_only true
       |> Config.put keep_assms false
+    val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
     val cprop =
-      Thm.cprem_of goal i
-      |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt
+      concl
+      |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt'
       |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
-    val irs = map (pair ~1) (Thm.assume cprop :: facts)
+    val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
     val rm = SOME run_remote
   in
     split_list xrules
-    ||> distinct (op =) o fst o smt_solver rm ctxt o append irs o map_index I
+    ||> distinct (op =) o fst o smt_solver rm ctxt' o append irs o map_index I
     |-> map_filter o try o nth
     |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
   end