src/HOL/Tools/inductive_package.ML
changeset 31174 f1f1e9b53c81
parent 30722 623d4831c8cf
child 31177 c39994cb152a
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat May 16 15:24:35 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat May 16 20:17:59 2009 +0200
     1.3 @@ -454,7 +454,7 @@
     1.4      val facts = args |> map (fn ((a, atts), props) =>
     1.5        ((a, map (prep_att thy) atts),
     1.6          map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
     1.7 -  in lthy |> LocalTheory.notes Thm.theoremK facts |>> map snd end;
     1.8 +  in lthy |> LocalTheory.notes Thm.generated_theoremK facts |>> map snd end;
     1.9  
    1.10  val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
    1.11  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
    1.12 @@ -849,7 +849,7 @@
    1.13        |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
    1.14      val (cs, ps) = chop (length cnames_syn) vars;
    1.15      val monos = Attrib.eval_thms lthy raw_monos;
    1.16 -    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
    1.17 +    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.generated_theoremK,
    1.18        alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
    1.19        skip_mono = false, fork_mono = not int};
    1.20    in