src/HOL/TPTP/mash_export.ML
changeset 75616 986506233812
parent 75612 03ae0ba2aa9e
child 76092 282f5e980a67
--- a/src/HOL/TPTP/mash_export.ML	Fri Jun 24 23:31:28 2022 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jun 24 23:38:41 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 |> Bytes.read |> Bytes.trim_split_lines
-    val mepo_lines = Path.explode mepo_file_name |> Bytes.read |> Bytes.trim_split_lines
+    val mash_lines = Path.explode mash_file_name |> File.read_lines
+    val mepo_lines = Path.explode mepo_file_name |> File.read_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"