| changeset 77851 | ec50b9213969 |
| parent 77850 | d589d1d218b2 |
| child 77910 | 10c09fb5a874 |
--- a/src/Pure/library.ML Fri Apr 14 22:08:16 2023 +0200 +++ b/src/Pure/library.ML Fri Apr 14 22:19:28 2023 +0200 @@ -771,7 +771,7 @@ val trim_split_lines = trim_line #> split_lines #> map trim_line; fun normalize_lines str = - if exists_string (fn s => s = "\r") str then + if member_string str "\r" then split_lines str |> map trim_line |> cat_lines else str;