diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/TPTP/TPTP_Parser.thy
--- a/src/HOL/TPTP/TPTP_Parser.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -6,16 +6,15 @@
 
 theory TPTP_Parser
 imports Pure
-uses
-  "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
+begin
+
+ML_file "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
 
-  "TPTP_Parser/tptp_syntax.ML"
-  "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*)
-  "TPTP_Parser/tptp_parser.ML"
-  "TPTP_Parser/tptp_problem_name.ML"
-  "TPTP_Parser/tptp_proof.ML"
-
-begin
+ML_file "TPTP_Parser/tptp_syntax.ML"
+ML_file "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*)
+ML_file "TPTP_Parser/tptp_parser.ML"
+ML_file "TPTP_Parser/tptp_problem_name.ML"
+ML_file "TPTP_Parser/tptp_proof.ML"
 
 text {*The TPTP parser was generated using ML-Yacc, and needs the
 ML-Yacc library to operate.  This library is included with the parser,