--- 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);