1.1 --- a/src/HOL/IsaMakefile	Fri Nov 20 22:38:41 2009 +1100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Nov 20 15:34:11 2009 +0100
     1.3 @@ -103,7 +103,6 @@
     1.4    $(SRC)/Provers/hypsubst.ML \
     1.5    $(SRC)/Provers/quantifier1.ML \
     1.6    $(SRC)/Provers/splitter.ML \
     1.7 -  $(SRC)/Tools/Auto_Counterexample.thy \
     1.8    $(SRC)/Tools/Code/code_haskell.ML \
     1.9    $(SRC)/Tools/Code/code_ml.ML \
    1.10    $(SRC)/Tools/Code/code_preproc.ML \

     2.1 --- a/src/Tools/Auto_Counterexample.thy	Fri Nov 20 22:38:41 2009 +1100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,15 +0,0 @@
     2.4 -(*  Title:   Tools/Auto_Counterexample.thy
     2.5 -    Author:  Jasmin Blanchette, TU Muenchen
     2.6 -
     2.7 -Counterexample Search Unit (do not abbreviate!).
     2.8 -*)
     2.9 -
    2.10 -header {* Counterexample Search Unit *}
    2.11 -
    2.12 -theory Auto_Counterexample
    2.13 -imports Pure
    2.14 -uses
    2.15 -  "~~/src/Tools/auto_counterexample.ML"
    2.16 -begin
    2.17 -
    2.18 -end

     3.1 --- a/src/Tools/Code_Generator.thy	Fri Nov 20 22:38:41 2009 +1100
     3.2 +++ b/src/Tools/Code_Generator.thy	Fri Nov 20 15:34:11 2009 +0100
     3.3 @@ -5,8 +5,9 @@
     3.4  header {* Loading the code generator modules *}
     3.5  
     3.6  theory Code_Generator
     3.7 -imports Auto_Counterexample
     3.8 +imports Pure
     3.9  uses
    3.10 +  "~~/src/Tools/auto_counterexample.ML"
    3.11    "~~/src/Tools/value.ML"
    3.12    "~~/src/Tools/quickcheck.ML"
    3.13    "~~/src/Tools/Code/code_preproc.ML"