# HG changeset patch
# User wenzelm
# Date 1683536953 -7200
# Node ID 1de3db73618efff1d19a034d355f75e89d49030f
# Parent  e30a56be9c7bdfb154ad74760aa2a2617c5ed07f
tuned whitespace;

diff -r e30a56be9c7b -r 1de3db73618e src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun May 07 22:51:23 2023 +0200
+++ b/src/Pure/General/name_space.ML	Mon May 08 11:09:13 2023 +0200
@@ -134,7 +134,8 @@
 
 type internals = string list Long_Name.Chunks.T;  (*external name -> internal names*)
 
-val merge_internals : internals * internals -> internals = Long_Name.Chunks.merge_list (op =);
+val merge_internals : internals * internals -> internals =
+  Long_Name.Chunks.merge_list (op =);
 
 fun add_internals name xname : internals -> internals =
   Long_Name.Chunks.update_list (op =) (xname, name);