1.1 --- a/src/HOL/HOL.thy	Tue Nov 24 16:11:50 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Nov 24 17:19:33 2009 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4  imports Pure "~~/src/Tools/Code_Generator"
     1.5  uses
     1.6    ("Tools/hologic.ML")
     1.7 -  "~~/src/Tools/auto_solve.ML"
     1.8    "~~/src/Tools/IsaPlanner/zipper.ML"
     1.9    "~~/src/Tools/IsaPlanner/isand.ML"
    1.10    "~~/src/Tools/IsaPlanner/rw_tools.ML"

     2.1 --- a/src/Tools/Code_Generator.thy	Tue Nov 24 16:11:50 2009 +0100
     2.2 +++ b/src/Tools/Code_Generator.thy	Tue Nov 24 17:19:33 2009 +0100
     2.3 @@ -7,9 +7,10 @@
     2.4  theory Code_Generator
     2.5  imports Pure
     2.6  uses
     2.7 +  "~~/src/Tools/auto_solve.ML"
     2.8    "~~/src/Tools/auto_counterexample.ML"
     2.9 +  "~~/src/Tools/quickcheck.ML"
    2.10    "~~/src/Tools/value.ML"
    2.11 -  "~~/src/Tools/quickcheck.ML"
    2.12    "~~/src/Tools/Code/code_preproc.ML" 
    2.13    "~~/src/Tools/Code/code_thingol.ML"
    2.14    "~~/src/Tools/Code/code_printer.ML"

     3.1 --- a/src/Tools/auto_solve.ML	Tue Nov 24 16:11:50 2009 +0100
     3.2 +++ b/src/Tools/auto_solve.ML	Tue Nov 24 17:19:33 2009 +0100
     3.3 @@ -27,17 +27,17 @@
     3.4  
     3.5  val _ =
     3.6    ProofGeneralPgip.add_preference Preferences.category_tracing
     3.7 +    (Preferences.nat_pref auto_time_limit
     3.8 +      "auto-solve-time-limit"
     3.9 +      "Time limit for seeking automatic solutions (in milliseconds).");
    3.10 +
    3.11 +val _ =
    3.12 +  ProofGeneralPgip.add_preference Preferences.category_tracing
    3.13    (setmp_CRITICAL auto true (fn () =>
    3.14      Preferences.bool_pref auto
    3.15        "auto-solve"
    3.16        "Try to solve newly declared lemmas with existing theorems.") ());
    3.17  
    3.18 -val _ =
    3.19 -  ProofGeneralPgip.add_preference Preferences.category_tracing
    3.20 -    (Preferences.nat_pref auto_time_limit
    3.21 -      "auto-solve-time-limit"
    3.22 -      "Time limit for seeking automatic solutions (in milliseconds).");
    3.23 -
    3.24  
    3.25  (* hook *)
    3.26