diff -r 805b0c13607e -r b2a9853ec6dd src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri Oct 19 21:59:33 2001 +0200
+++ b/src/HOL/ROOT.ML	Fri Oct 19 22:00:08 2001 +0200
@@ -17,7 +17,6 @@
 use "hologic.ML";
 
 use "~~/src/Provers/simplifier.ML";
-use "~~/src/Provers/split_paired_all.ML";
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/hypsubst.ML";
 use "~~/src/Provers/induct_method.ML";