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