# HG changeset patch
# User wenzelm
# Date 1258727651 -3600
# Node ID ee995d52580d4597b981ee842a2390c8a350321f
# Parent  cad5c38373d856fb49c4b1b8d33f509b5bec6f44# Parent  082d9bc6992de4e9f1883eacc1e47b40e71959c7
merged

diff -r cad5c38373d8 -r ee995d52580d src/HOL/IsaMakefile
--- 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 \
diff -r cad5c38373d8 -r ee995d52580d src/Tools/Auto_Counterexample.thy
--- 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
diff -r cad5c38373d8 -r ee995d52580d src/Tools/Code_Generator.thy
--- 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"