author | wenzelm |
Thu, 29 Nov 2001 01:50:19 +0100 | |
changeset 12323 | e151ee6e820f |
parent 12322 | abf3d7aa09ea |
child 12324 | 5db4b4596d1a |
--- 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