src/HOL/TPTP/mash_eval.ML
changeset 75612 03ae0ba2aa9e
parent 75044 38e24aeeedb8
child 75616 986506233812
--- a/src/HOL/TPTP/mash_eval.ML	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Jun 24 10:55:23 2022 +0200
@@ -46,7 +46,7 @@
       perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/"
 
     val methods = "isar" :: map method_of_file_name file_names
-    val lines_of = Path.explode #> try File.read_lines #> these
+    val lines_of = Path.explode #> try (Bytes.read #> Bytes.trim_split_lines) #> these
     val liness0 = map lines_of file_names
     val num_lines = fold (Integer.max o length) liness0 0