src/HOL/Nominal/nominal_inductive.ML
changeset 31174 f1f1e9b53c81
parent 30435 e62d6ecab6ad
child 31177 c39994cb152a
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat May 16 15:24:35 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sat May 16 20:17:59 2009 +0200
     1.3 @@ -561,7 +561,7 @@
     1.4              (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
     1.5            else (strong_raw_induct RSN (2, rev_mp),
     1.6              [ind_case_names, RuleCases.consumes 1]);
     1.7 -        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.theoremK
     1.8 +        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generated_theoremK
     1.9            ((rec_qualified (Binding.name "strong_induct"),
    1.10              map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
    1.11            ctxt;
    1.12 @@ -569,12 +569,12 @@
    1.13            ProjectRule.projects ctxt (1 upto length names) strong_induct'
    1.14        in
    1.15          ctxt' |>
    1.16 -        LocalTheory.note Thm.theoremK
    1.17 +        LocalTheory.note Thm.generated_theoremK
    1.18            ((rec_qualified (Binding.name "strong_inducts"),
    1.19              [Attrib.internal (K ind_case_names),
    1.20               Attrib.internal (K (RuleCases.consumes 1))]),
    1.21             strong_inducts) |> snd |>
    1.22 -        LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) =>
    1.23 +        LocalTheory.notes Thm.generated_theoremK (map (fn ((name, elim), (_, cases)) =>
    1.24              ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
    1.25                [Attrib.internal (K (RuleCases.case_names (map snd cases))),
    1.26                 Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
    1.27 @@ -664,7 +664,7 @@
    1.28        end) atoms
    1.29    in
    1.30      ctxt |>
    1.31 -    LocalTheory.notes Thm.theoremK (map (fn (name, ths) =>
    1.32 +    LocalTheory.notes Thm.generated_theoremK (map (fn (name, ths) =>
    1.33          ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
    1.34            [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
    1.35        (names ~~ transp thss)) |> snd