--- a/src/HOL/IsaMakefile Sun May 13 09:23:27 2007 +0200
+++ b/src/HOL/IsaMakefile Sun May 13 18:15:21 2007 +0200
@@ -62,7 +62,8 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Pure/General/int.ML $(SRC)/Pure/General/rat.ML \
+ $(SRC)/Provers/Arith/abel_cancel.ML \
$(SRC)/Provers/Arith/assoc_fold.ML \
$(SRC)/Provers/Arith/cancel_div_mod.ML \
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \
--- a/src/HOL/ROOT.ML Sun May 13 09:23:27 2007 +0200
+++ b/src/HOL/ROOT.ML Sun May 13 18:15:21 2007 +0200
@@ -22,6 +22,8 @@
use "~~/src/Provers/classical.ML";
use "~~/src/Provers/blast.ML";
use "~~/src/Provers/clasimp.ML";
+use "~~/src/Pure/General/int.ML";
+use "~~/src/Pure/General/rat.ML";
use "~~/src/Provers/Arith/fast_lin_arith.ML";
use "~~/src/Provers/Arith/cancel_sums.ML";
use "~~/src/Provers/Arith/assoc_fold.ML";