misc cleanup of auto_solve and quickcheck:
tools are in src/Tools and loaded uniformly in HOL;
preferences are configured in their proper place -- despite old misleading comments in the source;
use predefined preferences categories;
setmp preferences in-place;

--- a/src/HOL/HOL.thy	Sat Apr 25 20:31:27 2009 +0200
+++ b/src/HOL/HOL.thy	Sat Apr 25 21:28:04 2009 +0200
@@ -8,6 +8,7 @@
 imports Pure "~~/src/Tools/Code_Generator"
 uses
   ("Tools/hologic.ML")
+  "~~/src/Tools/auto_solve.ML"
   "~~/src/Tools/IsaPlanner/zipper.ML"
   "~~/src/Tools/IsaPlanner/isand.ML"
   "~~/src/Tools/IsaPlanner/rw_tools.ML"
@@ -1921,7 +1922,7 @@
 quickcheck_params [size = 5, iterations = 50]
 
 
-subsection {* Nitpick hooks *}
+subsection {* Nitpick setup *}
 
 text {* This will be relocated once Nitpick is moved to HOL. *}
 
@@ -1947,10 +1948,14 @@
   val description = "introduction rules for (co)inductive predicates as needed by Nitpick"
 )
 *}
-setup {* Nitpick_Const_Def_Thms.setup
-         #> Nitpick_Const_Simp_Thms.setup
-         #> Nitpick_Const_Psimp_Thms.setup
-         #> Nitpick_Ind_Intro_Thms.setup *}
+
+setup {*
+  Nitpick_Const_Def_Thms.setup
+  #> Nitpick_Const_Simp_Thms.setup
+  #> Nitpick_Const_Psimp_Thms.setup
+  #> Nitpick_Ind_Intro_Thms.setup
+*}
+
 
 subsection {* Legacy tactics and ML bindings *}
 

--- a/src/HOL/IsaMakefile	Sat Apr 25 20:31:27 2009 +0200
+++ b/src/HOL/IsaMakefile	Sat Apr 25 21:28:04 2009 +0200
@@ -89,6 +89,7 @@
   $(SRC)/Tools/IsaPlanner/rw_tools.ML \
   $(SRC)/Tools/IsaPlanner/zipper.ML \
   $(SRC)/Tools/atomize_elim.ML \
+  $(SRC)/Tools/auto_solve.ML \
   $(SRC)/Tools/code/code_haskell.ML \
   $(SRC)/Tools/code/code_ml.ML \
   $(SRC)/Tools/code/code_name.ML \

--- a/src/Pure/IsaMakefile	Sat Apr 25 20:31:27 2009 +0200
+++ b/src/Pure/IsaMakefile	Sat Apr 25 21:28:04 2009 +0200
@@ -40,9 +40,8 @@
 
 Pure: $(OUT)/Pure
 
-$(OUT)/Pure: $(BOOTSTRAP_FILES) \
-  Concurrent/ROOT.ML Concurrent/future.ML	\
-  Concurrent/mailbox.ML Concurrent/par_list.ML				\
+$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/ROOT.ML			\
+  Concurrent/future.ML Concurrent/mailbox.ML Concurrent/par_list.ML	\
   Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
   Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML	\
   General/alist.ML General/antiquote.ML General/balanced_tree.ML	\
@@ -87,7 +86,7 @@
   Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML		\
   Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML	\
   Thy/thy_output.ML Thy/thy_syntax.ML Tools/ROOT.ML			\
-  Tools/auto_solve.ML Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML	\
+  Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML	\
   Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
   conjunction.ML consts.ML context.ML context_position.ML conv.ML	\
   defs.ML display.ML drule.ML envir.ML facts.ML goal.ML			\

--- a/src/Pure/ProofGeneral/ROOT.ML	Sat Apr 25 20:31:27 2009 +0200
+++ b/src/Pure/ProofGeneral/ROOT.ML	Sat Apr 25 21:28:04 2009 +0200
@@ -14,11 +14,7 @@
 
 use "pgip_isabelle.ML";
 
-(use
-  |> setmp Proofterm.proofs 1
-  |> setmp quick_and_dirty true
-  |> setmp Quickcheck.auto true
-  |> setmp auto_solve true) "preferences.ML";
+use "preferences.ML";
 
 use "pgip_parser.ML";
 

--- a/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 20:31:27 2009 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 21:28:04 2009 +0200
@@ -6,6 +6,10 @@
 
 signature PREFERENCES =
 sig
+  val category_display: string
+  val category_advanced_display: string
+  val category_tracing: string
+  val category_proof: string
   type preference =
    {name: string,
     descr: string,
@@ -29,6 +33,14 @@
 structure Preferences: PREFERENCES =
 struct
 
+(* categories *)
+
+val category_display = "Display";
+val category_advanced_display = "Advanced Display";
+val category_tracing = "Tracing";
+val category_proof = "Proof"
+
+
 (* preferences and preference tables *)
 
 type preference =
@@ -66,11 +78,11 @@
 
 (* preferences of Pure *)
 
-val proof_pref =
+val proof_pref = setmp Proofterm.proofs 1 (fn () =>
   let
     fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
     fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
-  in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end;
+  in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
 
 val thm_depsN = "thm_deps";
 val thm_deps_pref =
@@ -145,24 +157,13 @@
   bool_pref Toplevel.debug
     "debugging"
     "Whether to enable debugging.",
-  bool_pref Quickcheck.auto
-    "auto-quickcheck"
-    "Whether to enable quickcheck automatically.",
-  nat_pref Quickcheck.auto_time_limit
-    "auto-quickcheck-time-limit"
-    "Time limit for automatic quickcheck (in milliseconds).",
-  bool_pref AutoSolve.auto
-    "auto-solve"
-    "Try to solve newly declared lemmas with existing theorems.",
-  nat_pref AutoSolve.auto_time_limit
-    "auto-solve-time-limit"
-    "Time limit for seeking automatic solutions (in milliseconds).",
   thm_deps_pref];
 
 val proof_preferences =
- [bool_pref quick_and_dirty
-    "quick-and-dirty"
-    "Take a few short cuts",
+ [setmp quick_and_dirty true (fn () =>
+    bool_pref quick_and_dirty
+      "quick-and-dirty"
+      "Take a few short cuts") (),
   bool_pref Toplevel.skip_proofs
     "skip-proofs"
     "Skip over proofs (interactive-only)",
@@ -175,10 +176,10 @@
     "Check proofs in parallel"];
 
 val pure_preferences =
- [("Display", display_preferences),
-  ("Advanced Display", advanced_display_preferences),
-  ("Tracing", tracing_preferences),
-  ("Proof", proof_preferences)];
+ [(category_display, display_preferences),
+  (category_advanced_display, advanced_display_preferences),
+  (category_tracing, tracing_preferences),
+  (category_proof, proof_preferences)];
 
 
 (* table of categories and preferences; names must be unique *)

--- a/src/Pure/Tools/auto_solve.ML	Sat Apr 25 20:31:27 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-(*  Title:      Tools/auto_solve.ML
-    Author:     Timothy Bourke and Gerwin Klein, NICTA
-
-Check whether a newly stated theorem can be solved directly by an
-existing theorem.  Duplicate lemmas can be detected in this way.
-
-The implementation is based in part on Berghofer and Haftmann's
-quickcheck.ML.  It relies critically on the FindTheorems solves
-feature.
-*)
-
-signature AUTO_SOLVE =
-sig
-  val auto : bool ref
-  val auto_time_limit : int ref
-  val limit : int ref
-
-  val seek_solution : bool -> Proof.state -> Proof.state
-end;
-
-structure AutoSolve : AUTO_SOLVE =
-struct
-
-val auto = ref false;
-val auto_time_limit = ref 2500;
-val limit = ref 5;
-
-fun seek_solution int state =
-  let
-    val ctxt = Proof.context_of state;
-
-    val crits = [(true, FindTheorems.Solves)];
-    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
-
-    fun prt_result (goal, results) =
-      let
-        val msg =
-          (case goal of
-            NONE => "The current goal"
-          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
-      in
-        Pretty.big_list
-          (msg ^ " could be solved directly with:")
-          (map (FindTheorems.pretty_thm ctxt) results)
-      end;
-
-    fun seek_against_goal () =
-      (case try Proof.get_goal state of
-        NONE => NONE
-      | SOME (_, (_, goal)) =>
-          let
-            val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
-            val rs =
-              if length subgoals = 1
-              then [(NONE, find goal)]
-              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
-            val results = filter_out (null o snd) rs;
-          in if null results then NONE else SOME results end);
-
-    fun go () =
-      let
-        val res =
-          TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
-            (try seek_against_goal) ();
-      in
-        (case res of
-          SOME (SOME results) =>
-            state |> Proof.goal_message
-              (fn () => Pretty.chunks
-                [Pretty.str "",
-                  Pretty.markup Markup.hilite
-                    (separate (Pretty.brk 0) (map prt_result results))])
-        | _ => state)
-      end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
-  in
-    if int andalso ! auto andalso not (! Toplevel.quiet)
-    then go ()
-    else state
-  end;
-
-end;
-
-val _ = Context.>> (Specification.add_theorem_hook AutoSolve.seek_solution);
-
-val auto_solve = AutoSolve.auto;
-val auto_solve_time_limit = AutoSolve.auto_time_limit;
-

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/auto_solve.ML	Sat Apr 25 21:28:04 2009 +0200
@@ -0,0 +1,101 @@
+(*  Title:      Tools/auto_solve.ML
+    Author:     Timothy Bourke and Gerwin Klein, NICTA
+
+Check whether a newly stated theorem can be solved directly by an
+existing theorem.  Duplicate lemmas can be detected in this way.
+
+The implementation is based in part on Berghofer and Haftmann's
+quickcheck.ML.  It relies critically on the FindTheorems solves
+feature.
+*)
+
+signature AUTO_SOLVE =
+sig
+  val auto : bool ref
+  val auto_time_limit : int ref
+  val limit : int ref
+end;
+
+structure AutoSolve : AUTO_SOLVE =
+struct
+
+(* preferences *)
+
+val auto = ref false;
+val auto_time_limit = ref 2500;
+val limit = ref 5;
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_tracing
+  (setmp auto true (fn () =>
+    Preferences.bool_pref auto
+      "auto-solve"
+      "Try to solve newly declared lemmas with existing theorems.") ());
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_tracing
+    (Preferences.nat_pref auto_time_limit
+      "auto-solve-time-limit"
+      "Time limit for seeking automatic solutions (in milliseconds).");
+
+
+(* hook *)
+
+val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
+  let
+    val ctxt = Proof.context_of state;
+
+    val crits = [(true, FindTheorems.Solves)];
+    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
+
+    fun prt_result (goal, results) =
+      let
+        val msg =
+          (case goal of
+            NONE => "The current goal"
+          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
+      in
+        Pretty.big_list
+          (msg ^ " could be solved directly with:")
+          (map (FindTheorems.pretty_thm ctxt) results)
+      end;
+
+    fun seek_against_goal () =
+      (case try Proof.get_goal state of
+        NONE => NONE
+      | SOME (_, (_, goal)) =>
+          let
+            val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
+            val rs =
+              if length subgoals = 1
+              then [(NONE, find goal)]
+              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
+            val results = filter_out (null o snd) rs;
+          in if null results then NONE else SOME results end);
+
+    fun go () =
+      let
+        val res =
+          TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
+            (try seek_against_goal) ();
+      in
+        (case res of
+          SOME (SOME results) =>
+            state |> Proof.goal_message
+              (fn () => Pretty.chunks
+                [Pretty.str "",
+                  Pretty.markup Markup.hilite
+                    (separate (Pretty.brk 0) (map prt_result results))])
+        | _ => state)
+      end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
+  in
+    if int andalso ! auto andalso not (! Toplevel.quiet)
+    then go ()
+    else state
+  end));
+
+end;
+
+val auto_solve = AutoSolve.auto;
+val auto_solve_time_limit = AutoSolve.auto_time_limit;
+

--- a/src/Tools/quickcheck.ML	Sat Apr 25 20:31:27 2009 +0200
+++ b/src/Tools/quickcheck.ML	Sat Apr 25 21:28:04 2009 +0200
@@ -6,16 +6,34 @@
 
 signature QUICKCHECK =
 sig
-  val test_term: Proof.context -> bool -> string option -> int -> int -> term -> (string * term) list option;
-  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
   val auto: bool ref
   val auto_time_limit: int ref
+  val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
+    (string * term) list option
+  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
 end;
 
 structure Quickcheck : QUICKCHECK =
 struct
 
-open Quickcheck; (*c.f. Pure/Tools/ROOT.ML*)
+(* preferences *)
+
+val auto = ref false;
+val auto_time_limit = ref 2500;
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_tracing
+  (setmp auto true (fn () =>
+    Preferences.bool_pref auto
+      "auto-quickcheck"
+      "Whether to enable quickcheck automatically.") ());
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_tracing
+    (Preferences.nat_pref auto_time_limit
+      "auto-quickcheck-time-limit"
+      "Time limit for automatic quickcheck (in milliseconds).");
+
 
 (* quickcheck configuration -- default parameters, test generators *)
 
@@ -140,7 +158,7 @@
 
 (* automatic testing *)
 
-fun test_goal_auto int state =
+val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
   let
     val ctxt = Proof.context_of state;
     val assms = map term_of (Assumption.all_assms_of ctxt);
@@ -161,12 +179,10 @@
     if int andalso !auto andalso not (!Toplevel.quiet)
     then test ()
     else state
-  end;
-
-val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);
+  end));
 
 
-(* Isar interfaces *)
+(* Isar commands *)
 
 fun read_nat s = case (Library.read_int o Symbol.explode) s
  of (k, []) => if k >= 0 then k