# HG changeset patch
# User blanchet
# Date 1280254563 -7200
# Node ID 479dfaae0b521340aa425620baa11c0be4ee80aa
# Parent  22dcaec5fa77eb224623d4601dc54be135cb3317
compile

diff -r 22dcaec5fa77 -r 479dfaae0b52 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jul 27 19:41:19 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jul 27 20:16:03 2010 +0200
@@ -283,7 +283,7 @@
     fun default_atp_name () =
       hd (#atps (Sledgehammer_Isar.default_params thy []))
       handle Empty => error "No ATP available."
-    fun get_prover name = (name, ATP_Manager.get_prover thy name)
+    fun get_prover name = (name, Sledgehammer.get_prover_fun thy name)
   in
     (case AList.lookup (op =) args proverK of
       SOME name => get_prover name
@@ -301,11 +301,11 @@
   let
     val {context = ctxt, facts, goal} = Proof.goal st
     val thy = ProofContext.theory_of ctxt
-    val change_dir = (fn SOME d => Config.put ATP_Systems.dest_dir d | _ => I)
+    val change_dir = (fn SOME d => Config.put Sledgehammer.dest_dir d | _ => I)
     val ctxt' =
       ctxt
       |> change_dir dir
-      |> Config.put ATP_Systems.measure_runtime true
+      |> Config.put Sledgehammer.measure_runtime true
     val params = Sledgehammer_Isar.default_params thy []
     val problem =
       {subgoal = 1, goal = (ctxt', (facts, goal)),
@@ -316,7 +316,7 @@
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     val ({outcome, message, used_thm_names,
-          atp_run_time_in_msecs = time_atp, ...}: ATP_Manager.prover_result,
+          atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.prover_result,
         time_isa) = time_limit (Mirabelle.cpu_time
                       (prover params (K "") (Time.fromSeconds timeout))) problem
   in