--- 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 *}
--- 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 *)