1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 21:11:44 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 29 19:40:56 2011 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4                        reraise exn
     1.5                      else
     1.6                        (unknownN, "Internal error:\n" ^
     1.7 -                                ML_Compiler.exn_message exn ^ "\n"))
     1.8 +                                 ML_Compiler.exn_message exn ^ "\n"))
     1.9          val _ =
    1.10            (* The "expect" argument is deliberately ignored if the prover is
    1.11               missing so that the "Metis_Examples" can be processed on any
    1.12 @@ -183,7 +183,7 @@
    1.13        end
    1.14      else
    1.15        (Async_Manager.launch das_tool birth_time death_time (desc ())
    1.16 -                            (apfst (curry (op <>) timeoutN) o go);
    1.17 +                            (apfst (curry (op =) someN) o go);
    1.18         (unknownN, state))
    1.19    end
    1.20  
    1.21 @@ -191,7 +191,8 @@
    1.22    ctxt |> select_smt_solver name
    1.23         |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
    1.24  
    1.25 -(* Makes backtraces more transparent and might be more efficient as well. *)
    1.26 +(* Makes backtraces more transparent and might well be more efficient as
    1.27 +   well. *)
    1.28  fun smart_par_list_map _ [] = []
    1.29    | smart_par_list_map f [x] = [f x]
    1.30    | smart_par_list_map f xs = Par_List.map f xs
    1.31 @@ -217,6 +218,7 @@
    1.32          state |> Proof.map_context (Config.put SMT_Config.verbose debug)
    1.33        val ctxt = Proof.context_of state
    1.34        val {facts = chained_ths, goal, ...} = Proof.goal state
    1.35 +      val chained_ths = chained_ths |> normalize_chained_theorems
    1.36        val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
    1.37        val _ = () |> not blocking ? kill_provers
    1.38        val _ = case find_first (not o is_prover_supported ctxt) provers of
    1.39 @@ -318,7 +320,7 @@
    1.40        val launch_ueq_atps =
    1.41          launch_atps "Unit equational provers" is_unit_equality ueq_atps
    1.42        fun launch_atps_and_smt_solvers () =
    1.43 -        [launch_full_atps, launch_ueq_atps, launch_smts]
    1.44 +        [launch_full_atps, launch_smts, launch_ueq_atps]
    1.45          |> smart_par_list_map (fn f => ignore (f (unknownN, state)))
    1.46          handle ERROR msg => (print ("Error: " ^ msg); error msg)
    1.47        fun maybe f (accum as (outcome_code, _)) =