1.1 --- a/src/FOL/Makefile	Tue Nov 09 11:02:01 1993 +0100
     1.2 +++ b/src/FOL/Makefile	Tue Nov 09 13:21:41 1993 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  BIN = $(ISABELLEBIN)
     1.6  COMP = $(ISABELLECOMP)
     1.7 -FILES =  ROOT.ML ifol.thy ifol.ML fol.thy fol.ML int-prover.ML simpdata.ML \
     1.8 +FILES =  ROOT.ML ifol.thy ifol.ML fol.thy fol.ML intprover.ML simpdata.ML \
     1.9  	../Provers/classical.ML ../Provers/simplifier.ML ../Provers/ind.ML
    1.10  
    1.11  $(BIN)/FOL:   $(BIN)/Pure  $(FILES) 

     2.1 --- a/src/FOL/ROOT.ML	Tue Nov 09 11:02:01 1993 +0100
     2.2 +++ b/src/FOL/ROOT.ML	Tue Nov 09 13:21:41 1993 +0100
     2.3 @@ -15,8 +15,8 @@
     2.4  open Readthy;
     2.5  
     2.6  print_depth 1;  
     2.7 -use_thy "ifol";
     2.8 -use_thy "fol";
     2.9 +use_thy "IFOL";
    2.10 +use_thy "FOL";
    2.11  
    2.12  use "../Provers/hypsubst.ML";
    2.13  use "../Provers/classical.ML";
    2.14 @@ -45,7 +45,7 @@
    2.15  structure Hypsubst = HypsubstFun(Hypsubst_Data);
    2.16  open Hypsubst;
    2.17  
    2.18 -use "int-prover.ML";
    2.19 +use "intprover.ML";
    2.20  
    2.21  (*** Applying ClassicalFun to create a classical prover ***)
    2.22  structure Classical_Data =