# HG changeset patch # User wenzelm # Date 1238438881 -7200 # Node ID ef13967f911fa4af1dc63c33b9ba270e6b6340d2 # Parent 1267011348116a60812709ee0a53f0b535e77273# Parent 04ebcd11add89f2c28a57c2866bb58780d2e6612 merged diff -r 126701134811 -r ef13967f911f src/Pure/General/binding.ML --- 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 *)