src/HOL/ROOT.ML

--- a/src/HOL/ROOT.ML	Thu Dec 02 10:36:20 2004 +0100
+++ b/src/HOL/ROOT.ML	Thu Dec 02 11:09:19 2004 +0100
@@ -39,14 +39,6 @@
 
 with_path "Integ" use_thy "Main";
 
-(*Linking to external resolution provers*)
-use "Tools/res_lib.ML";
-use "Tools/res_clause.ML";
-use "Tools/res_skolem_function.ML";
-use "Tools/res_axioms.ML";
-use "Tools/res_types_sorts.ML";
-use "Tools/res_atp.ML";
-
 path_add "~~/src/HOL/Library";
 
 print_depth 8;