--- a/src/Pure/library.ML Mon Apr 12 22:16:31 2021 +0200
+++ b/src/Pure/library.ML Mon Apr 12 22:17:48 2021 +0200
@@ -143,8 +143,6 @@
val cat_lines: string list -> string
val space_explode: string -> string -> string list
val split_lines: string -> string list
- val cat_strings0: string list -> string
- val split_strings0: string -> string list
val plain_words: string -> string
val prefix_lines: string -> string -> string
val prefix: string -> string -> string
@@ -741,9 +739,6 @@
val split_lines = space_explode "\n";
-val cat_strings0 = space_implode "\000";
-val split_strings0 = space_explode "\000";
-
fun plain_words s = space_explode "_" s |> space_implode " ";
fun prefix_lines "" txt = txt