src/HOL/Nominal/nominal_primrec.ML
changeset 24712 64ed05609568
parent 24707 dfeb98f84e93
child 24867 e5b55d7be9bb
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Sep 25 15:34:35 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Sep 25 17:06:14 2007 +0200
     1.3 @@ -275,7 +275,7 @@
     1.4        if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
     1.5      val (defs_thms', thy') =
     1.6        thy
     1.7 -      |> Theory.add_path primrec_name
     1.8 +      |> Sign.add_path primrec_name
     1.9        |> fold_map def (map (fn ((name, t), _) => ((name, []), t)) defs');
    1.10      val cert = cterm_of thy';
    1.11  
    1.12 @@ -369,7 +369,7 @@
    1.13             thy'
    1.14             |> note (("simps", [Simplifier.simp_add]), simps'')
    1.15             |> snd
    1.16 -           |> Theory.parent_path
    1.17 +           |> Sign.parent_path
    1.18           end))
    1.19        [goals] |>
    1.20      Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ =>