--- a/src/HOL/IsaMakefile Fri Nov 20 22:38:41 2009 +1100
+++ b/src/HOL/IsaMakefile Fri Nov 20 15:34:11 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 22:38:41 2009 +1100
+++ /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 22:38:41 2009 +1100
+++ b/src/Tools/Code_Generator.thy Fri Nov 20 15:34:11 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"