# HG changeset patch
# User blanchet
# Date 1361369558 -3600
# Node ID 20f6d400cc68ee2c6669d3471cd464e6b4c56960
# Parent  4c6ae305462e7580c9e7cde7f78dadce210a5361
don't pass chained facts directly to SMT solvers -- this breaks various invariants and is never necessary

diff -r 4c6ae305462e -r 20f6d400cc68 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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