src/Tools/auto_tools.ML

-(*  Title:      Tools/auto_counterexample.ML
+(*  Title:      Tools/auto_tools.ML
     Author:     Jasmin Blanchette, TU Muenchen
 
-Counterexample Search Unit (do not abbreviate!).
+Manager for tools that should be run automatically on newly entered conjectures.
 *)
 
-signature AUTO_COUNTEREXAMPLE =
+signature AUTO_TOOLS =
 sig
   val time_limit: int Unsynchronized.ref
 
   val register_tool :
     string * (Proof.state -> bool * Proof.state) -> theory -> theory
 end;
 
-structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
+structure Auto_Tools : AUTO_TOOLS =
 struct
 
 (* preferences *)
 
 val time_limit = Unsynchronized.ref 2500
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
     (Preferences.nat_pref time_limit
-      "auto-counterexample-time-limit"
-      "Time limit for automatic counterexample search (in milliseconds).")
+      "auto-tools-time-limit"
+      "Time limit for automatic tools (in milliseconds).")
 
 
 (* configuration *)
 
 structure Data = Theory_Data

               fold_rev (fn (_, tool) => fn (true, state) => (true, state)
                                          | (false, state) => tool state)
                    (Data.get (Proof.theory_of state)) (false, state) |> snd
             else
               state) ()
-    handle TimeLimit.TimeOut =>
-           (warning "Automatic counterexample search timed out."; state)))
+    handle TimeLimit.TimeOut => state))
 
 end;