--- 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];