--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Dec 17 12:02:57 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Dec 17 12:10:08 2010 +0100
@@ -498,8 +498,8 @@
val _ =
if debug then Output.urgent_message "Invoking SMT solver..." else ()
val (outcome, used_facts) =
- SMT_Solver.smt_filter_head iter_timeout state facts i
- |> SMT_Solver.smt_filter_tail remote
+ SMT_Solver.smt_filter_head state facts i
+ |> SMT_Solver.smt_filter_tail iter_timeout remote
|> (fn {outcome, used_facts} => (outcome, used_facts))
handle exn => if Exn.is_interrupt exn then
reraise exn