# HG changeset patch
# User wenzelm
# Date 1006995019 -3600
# Node ID e151ee6e820fee6fbeac85d247a3c22708f459f0
# Parent  abf3d7aa09eabb01589339d23534847e9475e67c
qualify_elem: do not qualify empty names ("");

diff -r abf3d7aa09ea -r e151ee6e820f src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Nov 29 01:49:44 2001 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Nov 29 01:50:19 2001 +0100
@@ -227,8 +227,9 @@
 
 fun qualify_elem prfx elem =
   let
-    fun qualify ((name, atts), x) =
-      ((NameSpace.pack (filter_out (equal "") (prfx @ [name])), atts), x);
+    fun qualify (arg as ((name, atts), x)) =
+      if name = "" then arg
+      else ((NameSpace.pack (filter_out (equal "") (prfx @ [name])), atts), x);
   in
     (case elem of
       Fixes fixes => Fixes fixes