diff -r e0d509b1df1d -r a52907967bae src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Jan 06 18:18:12 2006 +0100
+++ b/src/FOL/FOL.thy	Fri Jan 06 18:18:13 2006 +0100
@@ -8,8 +8,6 @@
 theory FOL
 imports IFOL
 uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
-      ("eqrule_FOL_data.ML")
-      ("~~/src/Provers/eqsubst.ML")
 begin
 
 
@@ -45,13 +43,6 @@
 setup "Simplifier.method_setup Splitter.split_modifiers"
 setup Splitter.setup
 setup Clasimp.setup
-
-
-subsection {* Lucas Dixon's eqstep tactic *}
-
-use "~~/src/Provers/eqsubst.ML";
-use "eqrule_FOL_data.ML";
-
 setup EqSubst.setup