src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 32865 f8d1e16ec758
parent 32864 a226f29d4bdc
parent 32863 5e8cef567042
child 32936 9491bec20595
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sat Oct 03 12:05:40 2009 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sat Oct 03 12:10:16 2009 +0200
     1.3 @@ -91,7 +91,6 @@
     1.4  );
     1.5  
     1.6  fun lookup_thread xs = AList.lookup Thread.equal xs;
     1.7 -fun delete_thread xs = AList.delete Thread.equal xs;
     1.8  fun update_thread xs = AList.update Thread.equal xs;
     1.9  
    1.10  
    1.11 @@ -117,7 +116,8 @@
    1.12  (* unregister thread *)
    1.13  
    1.14  fun unregister (success, message) thread = Synchronized.change state
    1.15 -  (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
    1.16 +  (fn state as
    1.17 +      State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
    1.18      (case lookup_thread active thread of
    1.19        SOME (birthtime, _, description) =>
    1.20          let
    1.21 @@ -317,9 +317,11 @@
    1.22  fun print_provers thy = Pretty.writeln
    1.23    (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
    1.24  
    1.25 -fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
    1.26 -  NONE => NONE
    1.27 -| SOME (prover, _) => SOME prover;
    1.28 +fun get_prover name thy =
    1.29 +  (case Symtab.lookup (Provers.get thy) name of
    1.30 +    NONE => NONE
    1.31 +  | SOME (prover, _) => SOME prover);
    1.32 +
    1.33  
    1.34  (* start prover thread *)
    1.35