# HG changeset patch
# User wenzelm
# Date 1238438967 -7200
# Node ID 09306de1d99d06f6802a0d6fc2eabe9c6491272d
# Parent  36b41d297d654aa5003777acc35aa0e3e728fa0f# Parent  ef13967f911fa4af1dc63c33b9ba270e6b6340d2
merged

diff -r 36b41d297d65 -r 09306de1d99d src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Mar 30 19:11:16 2009 +0200
+++ b/src/HOL/Int.thy	Mon Mar 30 20:49:27 2009 +0200
@@ -12,7 +12,7 @@
 uses
   ("Tools/numeral.ML")
   ("Tools/numeral_syntax.ML")
-  ("~~/src/Provers/Arith/assoc_fold.ML")
+  "~~/src/Provers/Arith/assoc_fold.ML"
   "~~/src/Provers/Arith/cancel_numerals.ML"
   "~~/src/Provers/Arith/combine_numerals.ML"
   ("Tools/int_arith.ML")
@@ -1525,7 +1525,6 @@
 lemmas zle_int = of_nat_le_iff [where 'a=int]
 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
 
-use "~~/src/Provers/Arith/assoc_fold.ML"
 use "Tools/int_arith.ML"
 declaration {* K Int_Arith.setup *}
 
diff -r 36b41d297d65 -r 09306de1d99d src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Mon Mar 30 19:11:16 2009 +0200
+++ b/src/Pure/General/binding.ML	Mon Mar 30 20:49:27 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 *)