src/HOL/Tools/ATP_Manager/atp_manager.ML

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Oct 02 22:15:30 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Oct 02 23:15:36 2009 +0200
@@ -95,7 +95,6 @@
 );
 
 fun lookup_thread xs = AList.lookup Thread.equal xs;
-fun delete_thread xs = AList.delete Thread.equal xs;
 fun update_thread xs = AList.update Thread.equal xs;
 
 
@@ -121,7 +120,8 @@
 (* unregister thread *)
 
 fun unregister (success, message) thread = Synchronized.change state
-  (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+  (fn state as
+      State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
     (case lookup_thread active thread of
       SOME (birthtime, _, description) =>
         let
@@ -326,9 +326,11 @@
 fun print_provers thy = Pretty.writeln
   (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
 
-fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
-  NONE => NONE
-| SOME (prover, _) => SOME prover;
+fun get_prover name thy =
+  (case Symtab.lookup (Provers.get thy) name of
+    NONE => NONE
+  | SOME (prover, _) => SOME prover);
+
 
 (* start prover thread *)