qualify_elem: do not qualify empty names ("");

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