unused;
authorwenzelm
Mon, 12 Apr 2021 22:17:48 +0200
changeset 73825 c5512fde6ad1
parent 73824 bdba138d462d
child 73826 e21aef453cd4
unused;
src/Pure/library.ML
--- 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