--- a/src/HOL/TPTP/ATP_Problem_Import.thy Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Tue Apr 24 09:47:40 2012 +0200
@@ -11,8 +11,6 @@
declare [[show_consts]] (* for Refute *)
-typedecl iota (* for TPTP *)
-
use "atp_problem_import.ML"
end