1.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Dec 17 12:02:57 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Dec 17 12:10:08 2010 +0100
     1.3 @@ -35,9 +35,9 @@
     1.4    (*filter*)
     1.5    type 'a smt_filter_head_result = 'a list * (int option * thm) list *
     1.6      (((int * thm) list * Proof.context) * (int * (int option * thm)) list)
     1.7 -  val smt_filter_head: Time.time -> Proof.state ->
     1.8 +  val smt_filter_head: Proof.state ->
     1.9      ('a * (int option * thm)) list -> int -> 'a smt_filter_head_result
    1.10 -  val smt_filter_tail: bool -> 'a smt_filter_head_result ->
    1.11 +  val smt_filter_tail: Time.time -> bool -> 'a smt_filter_head_result ->
    1.12      {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list}
    1.13  
    1.14    (*tactic*)
    1.15 @@ -325,12 +325,11 @@
    1.16  type 'a smt_filter_head_result = 'a list * (int option * thm) list *
    1.17    (((int * thm) list * Proof.context) * (int * (int option * thm)) list)
    1.18  
    1.19 -fun smt_filter_head time_limit st xwrules i =
    1.20 +fun smt_filter_head st xwrules i =
    1.21    let
    1.22      val ctxt =
    1.23        Proof.context_of st
    1.24        |> Config.put C.oracle false
    1.25 -      |> Config.put C.timeout (Time.toReal time_limit)
    1.26        |> Config.put C.drop_bad_facts true
    1.27        |> Config.put C.filter_only_facts true
    1.28  
    1.29 @@ -349,9 +348,13 @@
    1.30       |> `(gen_solver_head ctxt'))
    1.31    end
    1.32  
    1.33 -fun smt_filter_tail run_remote (xs, wthms, head as ((_, ctxt), _)) =
    1.34 -  let val xrules = xs ~~ map snd wthms in
    1.35 -    head
    1.36 +fun smt_filter_tail time_limit run_remote
    1.37 +    (xs, wthms, ((iwthms', ctxt), iwthms)) =
    1.38 +  let
    1.39 +    val ctxt = ctxt |> Config.put C.timeout (Time.toReal time_limit)
    1.40 +    val xrules = xs ~~ map snd wthms
    1.41 +  in
    1.42 +    ((iwthms', ctxt), iwthms)
    1.43      |-> gen_solver_tail (name_and_solver_of ctxt) (SOME run_remote)
    1.44      |> distinct (op =) o fst
    1.45      |> map_filter (try (nth xrules))

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