# HG changeset patch
# User blanchet
# Date 1335389959 -7200
# Node ID 53e30966b4b6dc4440d4bdc1acbc76ecae20a49b
# Parent  249a940953b045d26a5c4d46e436d6b784099df6
tuning

diff -r 249a940953b0 -r 53e30966b4b6 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