--- a/src/FOL/Makefile Tue Nov 09 11:02:01 1993 +0100
+++ b/src/FOL/Makefile Tue Nov 09 13:21:41 1993 +0100
@@ -18,7 +18,7 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-FILES = ROOT.ML ifol.thy ifol.ML fol.thy fol.ML int-prover.ML simpdata.ML \
+FILES = ROOT.ML ifol.thy ifol.ML fol.thy fol.ML intprover.ML simpdata.ML \
../Provers/classical.ML ../Provers/simplifier.ML ../Provers/ind.ML
$(BIN)/FOL: $(BIN)/Pure $(FILES)
--- a/src/FOL/ROOT.ML Tue Nov 09 11:02:01 1993 +0100
+++ b/src/FOL/ROOT.ML Tue Nov 09 13:21:41 1993 +0100
@@ -15,8 +15,8 @@
open Readthy;
print_depth 1;
-use_thy "ifol";
-use_thy "fol";
+use_thy "IFOL";
+use_thy "FOL";
use "../Provers/hypsubst.ML";
use "../Provers/classical.ML";
@@ -45,7 +45,7 @@
structure Hypsubst = HypsubstFun(Hypsubst_Data);
open Hypsubst;
-use "int-prover.ML";
+use "intprover.ML";
(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =