# HG changeset patch
# User blanchet
# Date 1272043012 -7200
# Node ID 20ef039bccff1f2c06920ae17ed51b6c53015cd6
# Parent  f32c567dbcaa1b06c0aa7e868dd44865f7173bc5
make "ATP_Manager.get_prover" a total function, since we always want to show the same error text

diff -r f32c567dbcaa -r 20ef039bccff src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Apr 23 19:12:49 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Apr 23 19:16:52 2010 +0200
@@ -53,7 +53,7 @@
   val running_atps: unit -> unit
   val messages: int option -> unit
   val add_prover: string * prover -> theory -> theory
-  val get_prover: theory -> string -> prover option
+  val get_prover: theory -> string -> prover
   val available_atps: theory -> unit
   val start_prover_thread:
     params -> Time.time -> Time.time -> int -> relevance_override
@@ -158,13 +158,13 @@
   Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
     (case lookup_thread active thread of
-      SOME (birth_time, _, description) =>
+      SOME (birth_time, _, desc) =>
         let
           val active' = delete_thread thread active;
           val now = Time.now ()
-          val cancelling' = (thread, (now, description)) :: cancelling;
+          val cancelling' = (thread, (now, desc)) :: cancelling;
           val message' =
-            description ^ "\n" ^ message ^
+            desc ^ "\n" ^ message ^
             (if verbose then
                "Total time: " ^ Int.toString (Time.toMilliseconds
                                           (Time.- (now, birth_time))) ^ " ms.\n"
@@ -308,7 +308,7 @@
 
 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name ^ ".");
 
-structure Provers = Theory_Data
+structure Data = Theory_Data
 (
   type T = (prover * stamp) Symtab.table;
   val empty = Symtab.empty;
@@ -318,44 +318,43 @@
 );
 
 fun add_prover (name, prover) thy =
-  Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
-    handle Symtab.DUP name => err_dup_prover name;
+  Data.map (Symtab.update_new (name, (prover, stamp ()))) thy
+  handle Symtab.DUP name => err_dup_prover name;
 
 fun get_prover thy name =
-  Option.map #1 (Symtab.lookup (Provers.get thy) name);
+  case Symtab.lookup (Data.get thy) name of
+    SOME (prover, _) => prover
+  | NONE => error ("Unknown ATP: " ^ name)
 
 fun available_atps thy =
   priority ("Available ATPs: " ^
-            commas (sort_strings (Symtab.keys (Provers.get thy))) ^ ".")
+            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
 
 
 (* start prover thread *)
 
 fun start_prover_thread (params as {timeout, ...}) birth_time death_time i
                         relevance_override minimize_command proof_state name =
-  (case get_prover (Proof.theory_of proof_state) name of
-    NONE => error ("Unknown ATP: " ^ quote name ^ ".")
-  | SOME prover =>
+  let
+    val prover = get_prover (Proof.theory_of proof_state) name
+    val {context = ctxt, facts, goal} = Proof.goal proof_state;
+    val n = Logic.count_prems (prop_of goal)
+    val desc =
+      "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
+        Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
+    val _ = Toplevel.thread true (fn () =>
       let
-        val {context = ctxt, facts, goal} = Proof.goal proof_state;
-        val n = Logic.count_prems (prop_of goal)
-        val desc =
-          "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
-            Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
-
-        val _ = Toplevel.thread true (fn () =>
-          let
-            val _ = register params birth_time death_time (Thread.self (), desc)
-            val problem =
-              {subgoal = i, goal = (ctxt, (facts, goal)),
-               relevance_override = relevance_override, axiom_clauses = NONE,
-               filtered_clauses = NONE}
-            val message =
-              #message (prover params (minimize_command name) timeout problem)
-              handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line i n []
-                   | ERROR msg => "Error: " ^ msg ^ ".\n";
-            val _ = unregister params message (Thread.self ());
-          in () end);
-      in () end);
+        val _ = register params birth_time death_time (Thread.self (), desc)
+        val problem =
+          {subgoal = i, goal = (ctxt, (facts, goal)),
+           relevance_override = relevance_override, axiom_clauses = NONE,
+           filtered_clauses = NONE}
+        val message =
+          #message (prover params (minimize_command name) timeout problem)
+          handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line i n []
+               | ERROR msg => "Error: " ^ msg ^ ".\n";
+        val _ = unregister params message (Thread.self ());
+      in () end)
+  in () end
 
 end;