--- a/src/HOL/TPTP/TPTP_Parser/tptp_parser.ML	Wed Aug 19 22:40:41 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_parser.ML	Thu Aug 20 13:41:53 2015 +0200
@@ -65,7 +65,7 @@
   fun parse_file' lookahead file_name =
     parse_expression
      file_name
-     (File.open_input TextIO.inputAll (Path.explode file_name))
+     (File.read (Path.explode file_name))
 end
 
 val parse_file = parse_file' LOOKAHEAD