| changeset 75616 | 986506233812 |
| parent 75612 | 03ae0ba2aa9e |
| child 79336 | 032a31db4c6f |
--- a/src/HOL/Import/import_rule.ML Fri Jun 24 23:31:28 2022 +0200 +++ b/src/HOL/Import/import_rule.ML Fri Jun 24 23:38:41 2022 +0200 @@ -441,7 +441,7 @@ 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"