load ML directly into theory Code_Generator (quickcheck also requires this);

--- a/src/HOL/IsaMakefile	Fri Nov 20 10:40:30 2009 +0100
+++ b/src/HOL/IsaMakefile	Fri Nov 20 15:33:10 2009 +0100
@@ -103,7 +103,6 @@
   $(SRC)/Provers/hypsubst.ML \
   $(SRC)/Provers/quantifier1.ML \
   $(SRC)/Provers/splitter.ML \
-  $(SRC)/Tools/Auto_Counterexample.thy \
   $(SRC)/Tools/Code/code_haskell.ML \
   $(SRC)/Tools/Code/code_ml.ML \
   $(SRC)/Tools/Code/code_preproc.ML \

--- a/src/Tools/Auto_Counterexample.thy	Fri Nov 20 10:40:30 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:   Tools/Auto_Counterexample.thy
-    Author:  Jasmin Blanchette, TU Muenchen
-
-Counterexample Search Unit (do not abbreviate!).
-*)
-
-header {* Counterexample Search Unit *}
-
-theory Auto_Counterexample
-imports Pure
-uses
-  "~~/src/Tools/auto_counterexample.ML"
-begin
-
-end

--- a/src/Tools/Code_Generator.thy	Fri Nov 20 10:40:30 2009 +0100
+++ b/src/Tools/Code_Generator.thy	Fri Nov 20 15:33:10 2009 +0100
@@ -5,8 +5,9 @@
 header {* Loading the code generator modules *}
 
 theory Code_Generator
-imports Auto_Counterexample
+imports Pure
 uses
+  "~~/src/Tools/auto_counterexample.ML"
   "~~/src/Tools/value.ML"
   "~~/src/Tools/quickcheck.ML"
   "~~/src/Tools/Code/code_preproc.ML"