src/HOL/ATP_Linkup.thy
changeset 23519 a4ffa756d8eb
parent 23444 6d4703843f93
child 23878 bd651ecd4b8a
--- a/src/HOL/ATP_Linkup.thy	Fri Jun 29 16:05:00 2007 +0200
+++ b/src/HOL/ATP_Linkup.thy	Fri Jun 29 18:21:25 2007 +0200
@@ -15,7 +15,7 @@
   ("Tools/res_hol_clause.ML")
   ("Tools/res_axioms.ML")
   ("Tools/res_reconstruct.ML")
-  ("Tools/ATP/watcher.ML")
+  ("Tools/watcher.ML")
   ("Tools/res_atp.ML")
   ("Tools/res_atp_provers.ML")
   ("Tools/res_atp_methods.ML")
@@ -88,7 +88,7 @@
 use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
 use "Tools/res_hol_clause.ML"  --{*requires the combinators*}
 use "Tools/res_reconstruct.ML"
-use "Tools/ATP/watcher.ML"
+use "Tools/watcher.ML"
 use "Tools/res_atp.ML"
 
 setup ResAxioms.meson_method_setup