diff -r f6d9e0e0b153 -r 1de908189869 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Dec 03 21:00:39 2008 -0800
+++ b/src/HOL/Tools/record_package.ML	Thu Dec 04 14:43:33 2008 +0100
@@ -1762,8 +1762,8 @@
     val external_names = NameSpace.external_names (Sign.naming_of thy);
 
     val alphas = map fst args;
-    val name = Sign.full_name thy bname;
-    val full = Sign.full_name_path thy bname;
+    val name = Sign.full_bname thy bname;
+    val full = Sign.full_bname_path thy bname;
     val base = Sign.base_name;
 
     val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
@@ -2253,7 +2253,7 @@
 
     (* errors *)
 
-    val name = Sign.full_name thy bname;
+    val name = Sign.full_bname thy bname;
     val err_dup_record =
       if is_none (get_record thy name) then []
       else ["Duplicate definition of record " ^ quote name];