--- a/src/FOLP/Makefile Tue Nov 09 13:21:41 1993 +0100
+++ b/src/FOLP/Makefile Tue Nov 09 13:25:07 1993 +0100
@@ -18,7 +18,7 @@
BIN = $(ISABELLEBIN)
COMP = $(ISABELLECOMP)
-FILES = ROOT.ML ifolp.thy ifolp.ML folp.thy folp.ML int-prover.ML simpdata.ML\
+FILES = ROOT.ML ifolp.thy ifolp.ML folp.thy folp.ML intprover.ML simpdata.ML\
classical.ML ../Provers/simp.ML ../Provers/ind.ML
$(BIN)/FOLP: $(BIN)/Pure $(FILES)
--- a/src/FOLP/ROOT.ML Tue Nov 09 13:21:41 1993 +0100
+++ b/src/FOLP/ROOT.ML Tue Nov 09 13:25:07 1993 +0100
@@ -16,8 +16,8 @@
open Readthy;
print_depth 1;
-use_thy "ifolp";
-use_thy "folp";
+use_thy "IFOLP";
+use_thy "FOLP";
use "../Provers/hypsubst.ML";
use "classical.ML"; (* Patched 'cos matching won't instantiate proof *)
@@ -47,7 +47,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 =