src/HOL/TPTP/TPTP_Interpret.thy

--- a/src/HOL/TPTP/TPTP_Interpret.thy	Tue Aug 05 14:02:47 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Interpret.thy	Tue Aug 05 15:54:47 2014 +0200
@@ -6,12 +6,12 @@
 *)
 
 theory TPTP_Interpret
-imports Main TPTP_Parser
+imports Complex_Main TPTP_Parser
 keywords "import_tptp" :: thy_decl
 begin
 
-typedecl "ind"
+typedecl ind
 
-ML_file  "TPTP_Parser/tptp_interpret.ML"
+ML_file "TPTP_Parser/tptp_interpret.ML"
 
 end
\ No newline at end of file