diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/old_primrec_package.ML
--- a/src/HOL/Tools/old_primrec_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -212,7 +212,7 @@
                     ((map snd ls) @ [dummyT])
                     (list_comb (Const (rec_name, dummyT),
                                 fs @ map Bound (0 ::(length ls downto 1))))
-    val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
+    val def_name = NameSpace.base_name fname ^ "_" ^ NameSpace.base_name tname ^ "_def";
     val def_prop =
       singleton (Syntax.check_terms (ProofContext.init thy))
         (Logic.mk_equals (Const (fname, dummyT), rhs));
@@ -269,7 +269,7 @@
             else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
               "\nare not mutually recursive");
     val primrec_name =
-      if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
+      if alt_name = "" then (space_implode "_" (map (NameSpace.base_name o #1) defs)) else alt_name;
     val (defs_thms', thy') =
       thy
       |> Sign.add_path primrec_name