# HG changeset patch
# User krauss
# Date 1207678476 -7200
# Node ID 9f81ab1b7b64f447937af5d2b09d8692717d0981
# Parent  6f9c62d17baa33b4c3862e0f1fbc371559179ded
fixed makefiles

diff -r 6f9c62d17baa -r 9f81ab1b7b64 src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Tue Apr 08 20:09:54 2008 +0200
+++ b/src/FOL/IsaMakefile	Tue Apr 08 20:14:36 2008 +0200
@@ -35,7 +35,7 @@
   $(SRC)/Tools/IsaPlanner/rw_tools.ML	\
   $(SRC)/Tools/IsaPlanner/rw_inst.ML \
   $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
-  $(SRC)/Tools/induct.ML			\
+  $(SRC)/Tools/induct.ML $(SRC)/Tools/atomize_elim.ML \
   $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
   $(SRC)/Provers/splitter.ML FOL.thy IFOL.thy ROOT.ML blastdata.ML cladata.ML 		\
   document/root.tex fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
diff -r 6f9c62d17baa -r 9f81ab1b7b64 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Apr 08 20:09:54 2008 +0200
+++ b/src/HOL/IsaMakefile	Tue Apr 08 20:14:36 2008 +0200
@@ -90,7 +90,7 @@
   $(SRC)/Provers/trancl.ML $(SRC)/Tools/Metis/metis.ML			\
   $(SRC)/Tools/code/code_funcgr.ML $(SRC)/Tools/code/code_name.ML	\
   $(SRC)/Tools/code/code_package.ML $(SRC)/Tools/code/code_target.ML	\
-  $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML			\
+  $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML \
   $(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy	\
   Accessible_Part.thy Arith_Tools.thy Code_Setup.thy Datatype.thy 			\
   Divides.thy Equiv_Relations.thy Extraction.thy	\