1.1 --- a/src/HOL/IsaMakefile	Wed Jul 06 17:19:34 2011 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jul 06 17:19:34 2011 +0100
     1.3 @@ -169,6 +169,7 @@
     1.4    $(SRC)/Provers/trancl.ML \
     1.5    $(SRC)/Tools/Metis/metis.ML \
     1.6    $(SRC)/Tools/rat.ML \
     1.7 +  ATP.thy \
     1.8    Complete_Lattice.thy \
     1.9    Complete_Partial_Order.thy \
    1.10    Datatype.thy \
    1.11 @@ -195,6 +196,12 @@
    1.12    SAT.thy \
    1.13    Set.thy \
    1.14    Sum_Type.thy \
    1.15 +  Tools/ATP/atp_problem.ML \
    1.16 +  Tools/ATP/atp_proof.ML \
    1.17 +  Tools/ATP/atp_reconstruct.ML \
    1.18 +  Tools/ATP/atp_systems.ML \
    1.19 +  Tools/ATP/atp_translate.ML \
    1.20 +  Tools/ATP/atp_util.ML \
    1.21    Tools/Datatype/datatype.ML \
    1.22    Tools/Datatype/datatype_abs_proofs.ML \
    1.23    Tools/Datatype/datatype_aux.ML \
    1.24 @@ -256,7 +263,6 @@
    1.25  	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
    1.26  
    1.27  MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
    1.28 -  ATP.thy \
    1.29    Big_Operators.thy \
    1.30    Code_Evaluation.thy \
    1.31    Code_Numeral.thy \
    1.32 @@ -299,12 +305,6 @@
    1.33    $(SRC)/Provers/Arith/cancel_numerals.ML \
    1.34    $(SRC)/Provers/Arith/combine_numerals.ML \
    1.35    $(SRC)/Provers/Arith/extract_common_term.ML \
    1.36 -  Tools/ATP/atp_problem.ML \
    1.37 -  Tools/ATP/atp_proof.ML \
    1.38 -  Tools/ATP/atp_reconstruct.ML \
    1.39 -  Tools/ATP/atp_systems.ML \
    1.40 -  Tools/ATP/atp_translate.ML \
    1.41 -  Tools/ATP/atp_util.ML \
    1.42    Tools/choice_specification.ML \
    1.43    Tools/code_evaluation.ML \
    1.44    Tools/groebner.ML \