src/HOL/Nominal/nominal_inductive2.ML
changeset 31174 f1f1e9b53c81
parent 30763 6976521b4263
child 31177 c39994cb152a
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sat May 16 15:24:35 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat May 16 20:17:59 2009 +0200
     1.3 @@ -461,7 +461,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 @@ -469,7 +469,7 @@
    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))]),