src/HOL/Import/import_rule.ML

   in
     process tstate (parse_line str)
   end
 
 fun process_file path thy =
-  #1 (fold process_line (Bytes.trim_split_lines (Bytes.read path)) (thy, init_state))
+  #1 (fold process_line (File.read_lines path) (thy, init_state))
 
 val _ = Outer_Syntax.command \<^command_keyword>\<open>import_file\<close>
   "import a recorded proof file"
   (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))