don't pass chained facts directly to SMT solvers -- this breaks various invariants and is never necessary

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 20 14:47:19 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 20 15:12:38 2013 +0100
@@ -1065,10 +1065,8 @@
         val birth = Timer.checkRealTimer timer
         val _ =
           if debug then Output.urgent_message "Invoking SMT solver..." else ()
-        val state_facts = these (try (#facts o Proof.goal) state)
         val (outcome, used_facts) =
-          SMT_Solver.smt_filter_preprocess ctxt state_facts goal weighted_facts
-              i
+          SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
           |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
           |> (fn {outcome, used_facts} => (outcome, used_facts))
           handle exn => if Exn.is_interrupt exn then