diff -r 92e0ed53db25 -r c39994cb152a src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sun May 17 07:17:39 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon May 18 09:48:06 2009 +0200
@@ -461,7 +461,7 @@
             (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
           else (strong_raw_induct RSN (2, rev_mp),
             [ind_case_names, RuleCases.consumes 1]);
-        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generated_theoremK
+        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
           ((rec_qualified (Binding.name "strong_induct"),
             map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
           ctxt;
@@ -469,7 +469,7 @@
           ProjectRule.projects ctxt' (1 upto length names) strong_induct'
       in
         ctxt' |>
-        LocalTheory.note Thm.generated_theoremK
+        LocalTheory.note Thm.generatedK
           ((rec_qualified (Binding.name "strong_inducts"),
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (RuleCases.consumes 1))]),