some rearangement of load order to keep preferences adjacent -- slightly fragile;

--- a/src/HOL/HOL.thy	Tue Nov 24 16:11:50 2009 +0100
+++ b/src/HOL/HOL.thy	Tue Nov 24 17:19:33 2009 +0100
@@ -8,7 +8,6 @@
 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"

--- a/src/Tools/Code_Generator.thy	Tue Nov 24 16:11:50 2009 +0100
+++ b/src/Tools/Code_Generator.thy	Tue Nov 24 17:19:33 2009 +0100
@@ -7,9 +7,10 @@
 theory Code_Generator
 imports Pure
 uses
+  "~~/src/Tools/auto_solve.ML"
   "~~/src/Tools/auto_counterexample.ML"
+  "~~/src/Tools/quickcheck.ML"
   "~~/src/Tools/value.ML"
-  "~~/src/Tools/quickcheck.ML"
   "~~/src/Tools/Code/code_preproc.ML" 
   "~~/src/Tools/Code/code_thingol.ML"
   "~~/src/Tools/Code/code_printer.ML"

--- a/src/Tools/auto_solve.ML	Tue Nov 24 16:11:50 2009 +0100
+++ b/src/Tools/auto_solve.ML	Tue Nov 24 17:19:33 2009 +0100
@@ -27,17 +27,17 @@
 
 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).");
+
+val _ =
+  ProofGeneralPgip.add_preference Preferences.category_tracing
   (setmp_CRITICAL 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 *)