src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 24 10:55:23 2022 +0200
@@ -681,7 +681,7 @@
         time_state
       else
         (disk_time,
-         (case try File.read_lines path of
+         (case try (Bytes.trim_split_lines o Bytes.read) path of
            SOME (version' :: node_lines) =>
            let
              fun extract_line_and_add_node line =