diff -r b2f209258621 -r 9c3acd90063a 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