--- a/src/HOL/Nominal/nominal_primrec.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Sep 25 17:06:14 2007 +0200
@@ -275,7 +275,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 cert = cterm_of thy';
@@ -369,7 +369,7 @@
thy'
|> note (("simps", [Simplifier.simp_add]), simps'')
|> snd
- |> Theory.parent_path
+ |> Sign.parent_path
end))
[goals] |>
Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ =>