--- a/src/HOL/TPTP/TPTP_Parser.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser.thy Thu Mar 15 22:08:53 2012 +0100
@@ -9,6 +9,7 @@
theory TPTP_Parser
imports Main
+keywords "import_tptp" :: diag (* FIXME !? *)
uses
"TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)