# HG changeset patch
# User wenzelm
# Date 1660468810 -7200
# Node ID 657b2de27454d146f2ede9826bbf59caac346949
# Parent  9ce4cb8e3f77a44c63a0a74f2a94861a72401869
clarified signature: avoid confusing operation name (amending 8cf14d4ebec4);

diff -r 9ce4cb8e3f77 -r 657b2de27454 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Aug 13 23:47:08 2022 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sun Aug 14 11:20:10 2022 +0200
@@ -156,7 +156,7 @@
     val parents = Theory.parents_of thy;
     val _ =
       Export.export thy \<^path_binding>\<open>theory/parents\<close>
-        (XML.Encode.string (terminate_lines (map Context.theory_long_name parents)));
+        (XML.Encode.string (cat_lines (map Context.theory_long_name parents) ^ "\n"));
 
 
     (* spec rules *)
diff -r 9ce4cb8e3f77 -r 657b2de27454 src/Pure/library.ML
--- 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;