src/ZF/Tools/datatype_package.ML

--- a/src/ZF/Tools/datatype_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -74,7 +74,7 @@
                    Syntax.string_of_term_global thy t);
 
   val rec_names = map (#1 o dest_Const) rec_hds
-  val rec_base_names = map Sign.base_name rec_names
+  val rec_base_names = map NameSpace.base_name rec_names
   val big_rec_base_name = space_implode "_" rec_base_names
 
   val thy_path = thy |> Sign.add_path big_rec_base_name