diff -r 71a526ee569a -r 2e1636e45770 src/HOL/TPTP/ATP_Problem_Import.thy
--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Apr 27 14:07:31 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Apr 27 15:24:37 2012 +0200
@@ -3,10 +3,9 @@
 *)
 
 header {* ATP Problem Importer *}
-
 theory ATP_Problem_Import
 imports Complex_Main TPTP_Interpret
-uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
+uses "sledgehammer_tactics.ML"
      "atp_problem_import.ML"
 begin