--- a/src/HOL/Tools/primrec_package.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/primrec_package.ML Tue Sep 25 17:06:14 2007 +0200
@@ -285,7 +285,7 @@
if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
val (defs_thms', thy') =
thy
- |> Theory.add_path primrec_name
+ |> Sign.add_path primrec_name
|> fold_map def (map (fn (name, t) => ((name, []), t)) defs');
val rewrites = (map mk_meta_eq rec_rewrites) @ map snd defs_thms';
val _ = message ("Proving equations for primrec function(s) " ^
@@ -302,7 +302,7 @@
|> snd
|> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
|> snd
- |> Theory.parent_path
+ |> Sign.parent_path
|> pair simps''
end;