src/HOL/Tools/record_package.ML

--- a/src/HOL/Tools/record_package.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -439,8 +439,8 @@
 fun get_extT_fields thy T =
   let
     val ((name,Ts),moreT) = dest_recT T;
-    val recname = let val (nm::recn::rst) = rev (NameSpace.unpack name)
-                  in NameSpace.pack (rev (nm::rst)) end;
+    val recname = let val (nm::recn::rst) = rev (NameSpace.explode name)
+                  in NameSpace.implode (rev (nm::rst)) end;
     val midx = maxidx_of_typs (moreT::Ts);
     val varifyT = varifyT midx;
     val {records,extfields,...} = RecordsData.get thy;