src/HOL/TPTP/TPTP_Interpret.thy

--- a/src/HOL/TPTP/TPTP_Interpret.thy	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret.thy	Tue Apr 17 16:14:07 2012 +0100
@@ -8,8 +8,9 @@
 theory TPTP_Interpret
 imports Main TPTP_Parser
 keywords "import_tptp" :: thy_decl
-uses
-  "TPTP_Parser/tptp_interpret.ML"
+uses  ("TPTP_Parser/tptp_interpret.ML")
 
 begin
+typedecl "ind"
+use  "TPTP_Parser/tptp_interpret.ML"
 end
\ No newline at end of file