src/HOL/Tools/inductive_package.ML

   let
     val thy = ProofContext.theory_of lthy;
     val facts = args |> map (fn ((a, atts), props) =>
       ((a, map (prep_att thy) atts),
         map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
-  in lthy |> LocalTheory.notes Thm.generated_theoremK facts |>> map snd end;
+  in lthy |> LocalTheory.notes Thm.generatedK facts |>> map snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
 
 

     val ((vars, intrs), _) = lthy
       |> ProofContext.set_mode ProofContext.mode_abbrev
       |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
     val (cs, ps) = chop (length cnames_syn) vars;
     val monos = Attrib.eval_thms lthy raw_monos;
-    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.generated_theoremK,
+    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.generatedK,
       alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
       skip_mono = false, fork_mono = not int};
   in
     lthy
     |> LocalTheory.set_group (serial_string ())