merged
authorwenzelm
Mon, 30 Mar 2009 20:48:01 +0200
changeset 30797 ef13967f911f
parent 30796 126701134811 (current diff)
parent 30795 04ebcd11add8 (diff)
child 30799 09306de1d99d
merged
--- a/src/Pure/General/binding.ML	Mon Mar 30 10:47:41 2009 -0700
+++ b/src/Pure/General/binding.ML	Mon Mar 30 20:48:01 2009 +0200
@@ -84,8 +84,9 @@
       let val (qualifier, name) = split_last (Long_Name.explode s)
       in make_binding ([], map (rpair false) qualifier, name, Position.none) end;
 
-fun qualified_name_of (Binding {qualifier, name, ...}) =
-  Long_Name.implode (map #1 qualifier @ [name]);
+fun qualified_name_of (b as Binding {qualifier, name, ...}) =
+  if is_empty b then ""
+  else Long_Name.implode (map #1 qualifier @ [name]);
 
 
 (* system prefix *)