# HG changeset patch
# User blanchet
# Date 1284194100 -7200
# Node ID 05452dd66b2b471b4edbff617e40f96859f0ae0d
# Parent  ce5c6a8b03599d83e61541b7c2f889e095ec6da6
finished renaming "Auto_Counterexample" to "Auto_Tools"

diff -r ce5c6a8b0359 -r 05452dd66b2b src/HOL/Mutabelle/MutabelleExtra.thy
--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Sat Sep 11 10:28:44 2010 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Sat Sep 11 10:35:00 2010 +0200
@@ -29,7 +29,7 @@
 nitpick_params [timeout = 5 s, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
 refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
 *)
-ML {* Auto_Counterexample.time_limit := 10 *}
+ML {* Auto_Tools.time_limit := 10 *}
 
 
 text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
@@ -53,4 +53,4 @@
 ML {* Output.priority_fn := old_pr *}
 ML {* Output.warning_fn := old_wa *}
 
-end
\ No newline at end of file
+end
diff -r ce5c6a8b0359 -r 05452dd66b2b src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Sep 11 10:28:44 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Sep 11 10:35:00 2010 +0200
@@ -94,13 +94,13 @@
  (map_types (inst_type insts) (Mutabelle.freeze t));
 
 fun invoke_quickcheck quickcheck_generator thy t =
-  TimeLimit.timeLimit (Time.fromSeconds (! Auto_Counterexample.time_limit))
+  TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
       (fn _ =>
           case Quickcheck.gen_test_term (ProofContext.init_global thy) true (SOME quickcheck_generator)
                                     size iterations (preprocess thy [] t) of
             (NONE, (time_report, report)) => (NoCex, (time_report, report))
           | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
-  handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Counterexample.time_limit)], NONE))
+  handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
 
 fun quickcheck_mtd quickcheck_generator =
   ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator)
diff -r ce5c6a8b0359 -r 05452dd66b2b src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Sep 11 10:28:44 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Sep 11 10:35:00 2010 +0200
@@ -383,6 +383,6 @@
 fun auto_nitpick state =
   if not (!auto) then (false, state) else pick_nits [] true 1 0 state
 
-val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
+val setup = Auto_Tools.register_tool ("nitpick", auto_nitpick)
 
 end;
diff -r ce5c6a8b0359 -r 05452dd66b2b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Sep 11 10:28:44 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Sep 11 10:35:00 2010 +0200
@@ -313,7 +313,6 @@
                        (minimize_command [] 1) state
     end
 
-val setup =
-  Auto_Counterexample.register_tool ("sledgehammer", auto_sledgehammer)
+val setup = Auto_Tools.register_tool ("sledgehammer", auto_sledgehammer)
 
 end;
diff -r ce5c6a8b0359 -r 05452dd66b2b src/Tools/auto_tools.ML
--- a/src/Tools/auto_tools.ML	Sat Sep 11 10:28:44 2010 +0200
+++ b/src/Tools/auto_tools.ML	Sat Sep 11 10:35:00 2010 +0200
@@ -1,10 +1,10 @@
-(*  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
 
@@ -12,7 +12,7 @@
     string * (Proof.state -> bool * Proof.state) -> theory -> theory
 end;
 
-structure Auto_Counterexample : AUTO_COUNTEREXAMPLE =
+structure Auto_Tools : AUTO_TOOLS =
 struct
 
 (* preferences *)
@@ -22,8 +22,8 @@
 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 *)
@@ -53,7 +53,6 @@
                    (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;
diff -r ce5c6a8b0359 -r 05452dd66b2b src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sat Sep 11 10:28:44 2010 +0200
+++ b/src/Tools/quickcheck.ML	Sat Sep 11 10:35:00 2010 +0200
@@ -320,7 +320,7 @@
           Pretty.mark Markup.hilite (pretty_counterex ctxt cex)])) state)
     end
 
-val setup = Auto_Counterexample.register_tool ("quickcheck", auto_quickcheck)
+val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
 
 
 (* Isar commands *)