# HG changeset patch
# User wenzelm
# Date 1618258668 -7200
# Node ID c5512fde6ad1ae653ace8c8ce8477847fa1acdf4
# Parent  bdba138d462d70f0e4ae3df8f827fa0e8586afea
unused;

diff -r bdba138d462d -r c5512fde6ad1 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