src/HOL/TPTP/ATP_Problem_Import.thy

--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Apr 25 22:00:33 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Apr 25 23:39:19 2012 +0200
@@ -7,7 +7,7 @@
 theory ATP_Problem_Import
 imports Complex_Main TPTP_Interpret
 uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
-     ("atp_problem_import.ML")
+     "atp_problem_import.ML"
 begin
 
 ML {* Proofterm.proofs := 0 *}
@@ -15,6 +15,4 @@
 declare [[show_consts]] (* for Refute *)
 declare [[smt_oracle]]
 
-use "atp_problem_import.ML"
-
 end