--- a/src/Pure/library.ML Sat Aug 13 23:47:08 2022 +0200
+++ b/src/Pure/library.ML Sun Aug 14 11:20:10 2022 +0200
@@ -145,7 +145,6 @@
val commas: string list -> string
val commas_quote: string list -> string
val cat_lines: string list -> string
- val terminate_lines: string list -> string
val space_explode: string -> string -> string list
val split_lines: string -> string list
val plain_words: string -> string
@@ -749,8 +748,6 @@
val cat_lines = space_implode "\n";
-fun terminate_lines lines = cat_lines lines ^ "\n";
-
(*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)
fun space_explode _ "" = []
| space_explode sep s = String.fields (fn c => str c = sep) s;