--- a/src/ZF/Tools/primrec_package.ML Thu Mar 05 11:58:53 2009 +0100
+++ b/src/ZF/Tools/primrec_package.ML Thu Mar 05 12:08:00 2009 +0100
@@ -139,7 +139,7 @@
(** make definition **)
(*the recursive argument*)
- val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
+ val rec_arg = Free (Name.variant (map #1 (ls@rs)) (NameSpace.base_name big_rec_name),
Ind_Syntax.iT)
val def_tm = Logic.mk_equals
@@ -153,7 +153,7 @@
writeln ("primrec def:\n" ^
Syntax.string_of_term_global thy def_tm)
else();
- (Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
+ (NameSpace.base_name fname ^ "_" ^ NameSpace.base_name big_rec_name ^ "_def",
def_tm)
end;
@@ -168,7 +168,7 @@
val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
val ([def_thm], thy1) = thy
- |> Sign.add_path (Sign.base_name fname)
+ |> Sign.add_path (NameSpace.base_name fname)
|> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)