src/HOL/Import/import_rule.ML

--- a/src/HOL/Import/import_rule.ML	Thu Jun 23 23:42:47 2022 +0200
+++ b/src/HOL/Import/import_rule.ML	Fri Jun 24 10:55:23 2022 +0200
@@ -441,7 +441,7 @@
   end
 
 fun process_file path thy =
-  (thy, init_state) |> File.fold_lines process_line path |> fst
+  #1 (fold process_line (Bytes.trim_split_lines (Bytes.read path)) (thy, init_state))
 
 val _ = Outer_Syntax.command \<^command_keyword>\<open>import_file\<close>
   "import a recorded proof file"