--- a/src/HOL/TPTP/mash_export.ML Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Jun 24 10:55:23 2022 +0200
@@ -316,8 +316,8 @@
val mesh_line = encode_str name ^ ": " ^ encode_strs mesh_suggs ^ "\n"
in File.append mesh_path mesh_line end
- val mash_lines = Path.explode mash_file_name |> File.read_lines
- val mepo_lines = Path.explode mepo_file_name |> File.read_lines
+ val mash_lines = Path.explode mash_file_name |> Bytes.read |> Bytes.trim_split_lines
+ val mepo_lines = Path.explode mepo_file_name |> Bytes.read |> Bytes.trim_split_lines
in
if length mash_lines = length mepo_lines then List.app do_fact (mash_lines ~~ mepo_lines)
else warning "Skipped: MaSh file missing or out of sync with MePo file"