--- a/src/FOL/IsaMakefile Tue Jun 27 23:43:46 2000 +0200
+++ b/src/FOL/IsaMakefile Wed Jun 28 10:37:08 2000 +0200
@@ -26,7 +26,7 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML \
+$(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML \
$(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML FOL.ML \
--- a/src/FOL/ROOT.ML Tue Jun 27 23:43:46 2000 +0200
+++ b/src/FOL/ROOT.ML Wed Jun 28 10:37:08 2000 +0200
@@ -16,6 +16,7 @@
use "~~/src/Provers/splitter.ML";
use "~~/src/Provers/ind.ML";
use "~~/src/Provers/hypsubst.ML";
+use "~~/src/Provers/make_elim.ML";
use "~~/src/Provers/classical.ML";
use "~~/src/Provers/blast.ML";
use "~~/src/Provers/clasimp.ML";
--- a/src/HOL/IsaMakefile Tue Jun 27 23:43:46 2000 +0200
+++ b/src/HOL/IsaMakefile Wed Jun 28 10:37:08 2000 +0200
@@ -36,7 +36,8 @@
$(SRC)/Provers/Arith/assoc_fold.ML \
$(SRC)/Provers/Arith/combine_numerals.ML \
$(SRC)/Provers/Arith/cancel_numerals.ML \
- $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
+ $(SRC)/Provers/Arith/fast_lin_arith.ML \
+ $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \
$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
$(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
$(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
--- a/src/HOL/ROOT.ML Tue Jun 27 23:43:46 2000 +0200
+++ b/src/HOL/ROOT.ML Wed Jun 28 10:37:08 2000 +0200
@@ -20,6 +20,7 @@
use "~~/src/Provers/split_paired_all.ML";
use "~~/src/Provers/splitter.ML";
use "~~/src/Provers/hypsubst.ML";
+use "~~/src/Provers/make_elim.ML";
use "~~/src/Provers/classical.ML";
use "~~/src/Provers/blast.ML";
use "~~/src/Provers/clasimp.ML";