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

     2.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sat May 16 15:24:35 2009 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat May 16 20:17:59 2009 +0200
     2.3 @@ -461,7 +461,7 @@
     2.4              (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
     2.5            else (strong_raw_induct RSN (2, rev_mp),
     2.6              [ind_case_names, RuleCases.consumes 1]);
     2.7 -        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.theoremK
     2.8 +        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generated_theoremK
     2.9            ((rec_qualified (Binding.name "strong_induct"),
    2.10              map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
    2.11            ctxt;
    2.12 @@ -469,7 +469,7 @@
    2.13            ProjectRule.projects ctxt' (1 upto length names) strong_induct'
    2.14        in
    2.15          ctxt' |>
    2.16 -        LocalTheory.note Thm.theoremK
    2.17 +        LocalTheory.note Thm.generated_theoremK
    2.18            ((rec_qualified (Binding.name "strong_inducts"),
    2.19              [Attrib.internal (K ind_case_names),
    2.20               Attrib.internal (K (RuleCases.consumes 1))]),

     3.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat May 16 15:24:35 2009 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sat May 16 20:17:59 2009 +0200
     3.3 @@ -367,11 +367,11 @@
     3.4        (fn thss => fn goal_ctxt =>
     3.5           let
     3.6             val simps = ProofContext.export goal_ctxt lthy' (flat thss);
     3.7 -           val (simps', lthy'') = fold_map (LocalTheory.note Thm.theoremK)
     3.8 +           val (simps', lthy'') = fold_map (LocalTheory.note Thm.generated_theoremK)
     3.9               (names_atts' ~~ map single simps) lthy'
    3.10           in
    3.11             lthy''
    3.12 -           |> LocalTheory.note Thm.theoremK ((qualify (Binding.name "simps"),
    3.13 +           |> LocalTheory.note Thm.generated_theoremK ((qualify (Binding.name "simps"),
    3.14                  map (Attrib.internal o K)
    3.15                      [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
    3.16                  maps snd simps')

     4.1 --- a/src/HOL/String.thy	Sat May 16 15:24:35 2009 +0200
     4.2 +++ b/src/HOL/String.thy	Sat May 16 20:17:59 2009 +0200
     4.3 @@ -55,7 +55,7 @@
     4.4     (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
     4.5        nibbles nibbles;
     4.6  in
     4.7 -  PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
     4.8 +  PureThy.note_thmss Thm.generated_theoremK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
     4.9    #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    4.10  end
    4.11  *}

     5.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat May 16 15:24:35 2009 +0200
     5.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat May 16 20:17:59 2009 +0200
     5.3 @@ -45,7 +45,7 @@
     5.4       Nitpick_Const_Psimp_Thms.add]
     5.5  
     5.6  fun note_theorem ((name, atts), ths) =
     5.7 -  LocalTheory.note Thm.theoremK ((Binding.qualified_name name, atts), ths)
     5.8 +  LocalTheory.note Thm.generated_theoremK ((Binding.qualified_name name, atts), ths)
     5.9  
    5.10  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
    5.11  
    5.12 @@ -56,7 +56,7 @@
    5.13                     |> map (apfst (apfst extra_qualify))
    5.14  
    5.15        val (saved_spec_simps, lthy) =
    5.16 -        fold_map (LocalTheory.note Thm.theoremK) spec lthy
    5.17 +        fold_map (LocalTheory.note Thm.generated_theoremK) spec lthy
    5.18  
    5.19        val saved_simps = flat (map snd saved_spec_simps)
    5.20        val simps_by_f = sort saved_simps

     6.1 --- a/src/HOL/Tools/inductive_package.ML	Sat May 16 15:24:35 2009 +0200
     6.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat May 16 20:17:59 2009 +0200
     6.3 @@ -454,7 +454,7 @@
     6.4      val facts = args |> map (fn ((a, atts), props) =>
     6.5        ((a, map (prep_att thy) atts),
     6.6          map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
     6.7 -  in lthy |> LocalTheory.notes Thm.theoremK facts |>> map snd end;
     6.8 +  in lthy |> LocalTheory.notes Thm.generated_theoremK facts |>> map snd end;
     6.9  
    6.10  val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
    6.11  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
    6.12 @@ -849,7 +849,7 @@
    6.13        |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
    6.14      val (cs, ps) = chop (length cnames_syn) vars;
    6.15      val monos = Attrib.eval_thms lthy raw_monos;
    6.16 -    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
    6.17 +    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.generated_theoremK,
    6.18        alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
    6.19        skip_mono = false, fork_mono = not int};
    6.20    in

     7.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat May 16 15:24:35 2009 +0200
     7.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat May 16 20:17:59 2009 +0200
     7.3 @@ -349,7 +349,7 @@
     7.4  
     7.5      val (ind_info, thy3') = thy2 |>
     7.6        InductivePackage.add_inductive_global (serial_string ())
     7.7 -        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
     7.8 +        {quiet_mode = false, verbose = false, kind = Thm.generated_theoremK, alt_name = Binding.empty,
     7.9            coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
    7.10          rlzpreds rlzparams (map (fn (rintr, intr) =>
    7.11            ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),

     8.1 --- a/src/HOL/Tools/primrec_package.ML	Sat May 16 15:24:35 2009 +0200
     8.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat May 16 20:17:59 2009 +0200
     8.3 @@ -253,8 +253,8 @@
     8.4      |> set_group ? LocalTheory.set_group (serial_string ())
     8.5      |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
     8.6      |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
     8.7 -    |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
     8.8 -    |-> (fn simps' => LocalTheory.note Thm.theoremK
     8.9 +    |-> (fn simps => fold_map (LocalTheory.note Thm.generated_theoremK) simps)
    8.10 +    |-> (fn simps' => LocalTheory.note Thm.generated_theoremK
    8.11            ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps'))
    8.12      |>> snd
    8.13    end handle PrimrecError (msg, some_eqn) =>

     9.1 --- a/src/HOL/ex/predicate_compile.ML	Sat May 16 15:24:35 2009 +0200
     9.2 +++ b/src/HOL/ex/predicate_compile.ML	Sat May 16 20:17:59 2009 +0200
     9.3 @@ -1393,7 +1393,7 @@
     9.4      val (predname, _) = dest_Const pred
     9.5      fun after_qed [[th]] lthy'' =
     9.6        lthy''
     9.7 -      |> LocalTheory.note Thm.theoremK
     9.8 +      |> LocalTheory.note Thm.generated_theoremK
     9.9             ((Binding.empty, [Attrib.internal (K add_elim_attrib)]), [th])
    9.10        |> snd
    9.11        |> LocalTheory.theory (prove_equation predname NONE)

    10.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Sat May 16 15:24:35 2009 +0200
    10.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Sat May 16 20:17:59 2009 +0200
    10.3 @@ -195,7 +195,7 @@
    10.4      val unfold_thms = unfolds names tuple_unfold_thm;
    10.5      fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
    10.6      val (thmss, lthy'') = lthy'
    10.7 -      |> fold_map (LocalTheory.note Thm.theoremK o mk_note)
    10.8 +      |> fold_map (LocalTheory.note Thm.generated_theoremK o mk_note)
    10.9          ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
   10.10    in
   10.11      (lthy'', names, fixdef_thms, map snd unfold_thms)
   10.12 @@ -373,7 +373,7 @@
   10.13        val simps2 : (Attrib.binding * thm list) list =
   10.14          map (apsnd (fn thm => [thm])) (List.concat simps);
   10.15        val (_, lthy'') = lthy'
   10.16 -        |> fold_map (LocalTheory.note Thm.theoremK) (simps1 @ simps2);
   10.17 +        |> fold_map (LocalTheory.note Thm.generated_theoremK) (simps1 @ simps2);
   10.18      in
   10.19        lthy''
   10.20      end

    11.1 --- a/src/Pure/Isar/attrib.ML	Sat May 16 15:24:35 2009 +0200
    11.2 +++ b/src/Pure/Isar/attrib.ML	Sat May 16 20:17:59 2009 +0200
    11.3 @@ -123,7 +123,7 @@
    11.4  
    11.5  fun attribute thy = attribute_i thy o intern_src thy;
    11.6  
    11.7 -fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
    11.8 +fun eval_thms ctxt args = ProofContext.note_thmss Thm.generated_theoremK
    11.9      [(Thm.empty_binding, args |> map (fn (a, atts) =>
   11.10          (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
   11.11    |> fst |> maps snd;

    12.1 --- a/src/Pure/Thy/thm_deps.ML	Sat May 16 15:24:35 2009 +0200
    12.2 +++ b/src/Pure/Thy/thm_deps.ML	Sat May 16 20:17:59 2009 +0200
    12.3 @@ -66,7 +66,7 @@
    12.4        case Thm.get_group thm of
    12.5          NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
    12.6      val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
    12.7 -      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
    12.8 +      if member (op =) [Thm.theoremK, Thm.generated_theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
    12.9          andalso is_unused p
   12.10        then
   12.11          (case Thm.get_group thm of

    13.1 --- a/src/Pure/more_thm.ML	Sat May 16 15:24:35 2009 +0200
    13.2 +++ b/src/Pure/more_thm.ML	Sat May 16 20:17:59 2009 +0200
    13.3 @@ -70,6 +70,7 @@
    13.4    val assumptionK: string
    13.5    val definitionK: string
    13.6    val theoremK: string
    13.7 +  val generated_theoremK : string
    13.8    val lemmaK: string
    13.9    val corollaryK: string
   13.10    val internalK: string
   13.11 @@ -388,6 +389,7 @@
   13.12  val assumptionK = "assumption";
   13.13  val definitionK = "definition";
   13.14  val theoremK = "theorem";
   13.15 +val generated_theoremK = "generated_theoremK"
   13.16  val lemmaK = "lemma";
   13.17  val corollaryK = "corollary";
   13.18  val internalK = Markup.internalK;