# HG changeset patch
# User wenzelm
# Date 1258129509 -3600
# Node ID e49bfeb0d822ae19bd38c3a03908f017441c4d19
# Parent  bdcabcffaaf65a9bd1e57f340cfa7bef7708b865
eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);

diff -r bdcabcffaaf6 -r e49bfeb0d822 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -561,7 +561,7 @@
             (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
           else (strong_raw_induct RSN (2, rev_mp),
             [ind_case_names, Rule_Cases.consumes 1]);
-        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
+        val ((_, [strong_induct']), ctxt') = LocalTheory.note ""
           ((rec_qualified (Binding.name "strong_induct"),
             map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
           ctxt;
@@ -569,12 +569,12 @@
           Project_Rule.projects ctxt (1 upto length names) strong_induct'
       in
         ctxt' |>
-        LocalTheory.note Thm.generatedK
+        LocalTheory.note ""
           ((rec_qualified (Binding.name "strong_inducts"),
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (Rule_Cases.consumes 1))]),
            strong_inducts) |> snd |>
-        LocalTheory.notes Thm.generatedK (map (fn ((name, elim), (_, cases)) =>
+        LocalTheory.notes "" (map (fn ((name, elim), (_, cases)) =>
             ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
               [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
                Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
@@ -664,7 +664,7 @@
       end) atoms
   in
     ctxt |>
-    LocalTheory.notes Thm.generatedK (map (fn (name, ths) =>
+    LocalTheory.notes "" (map (fn (name, ths) =>
         ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
           [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
       (names ~~ transp thss)) |> snd
diff -r bdcabcffaaf6 -r e49bfeb0d822 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -466,7 +466,7 @@
             NONE => (rec_qualified (Binding.name "strong_induct"),
                      rec_qualified (Binding.name "strong_inducts"))
           | SOME s => (Binding.name s, Binding.name (s ^ "s"));
-        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
+        val ((_, [strong_induct']), ctxt') = LocalTheory.note ""
           ((induct_name,
             map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
           ctxt;
@@ -474,7 +474,7 @@
           Project_Rule.projects ctxt' (1 upto length names) strong_induct'
       in
         ctxt' |>
-        LocalTheory.note Thm.generatedK
+        LocalTheory.note ""
           ((inducts_name,
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (Rule_Cases.consumes 1))]),
diff -r bdcabcffaaf6 -r e49bfeb0d822 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -367,11 +367,11 @@
       (fn thss => fn goal_ctxt =>
          let
            val simps = ProofContext.export goal_ctxt lthy' (flat thss);
-           val (simps', lthy'') = fold_map (LocalTheory.note Thm.generatedK)
+           val (simps', lthy'') = fold_map (LocalTheory.note "")
              (names_atts' ~~ map single simps) lthy'
          in
            lthy''
-           |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
+           |> LocalTheory.note "" ((qualify (Binding.name "simps"),
                 map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
                 maps snd simps')
            |> snd
diff -r bdcabcffaaf6 -r e49bfeb0d822 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -44,7 +44,7 @@
      Nitpick_Psimps.add]
 
 fun note_theorem ((binding, atts), ths) =
-  LocalTheory.note Thm.generatedK ((binding, atts), ths)
+  LocalTheory.note "" ((binding, atts), ths)
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 
@@ -55,7 +55,7 @@
                    |> map (apfst (apfst extra_qualify))
 
       val (saved_spec_simps, lthy) =
-        fold_map (LocalTheory.note Thm.generatedK) spec lthy
+        fold_map (LocalTheory.note "") spec lthy
 
       val saved_simps = maps snd saved_spec_simps
       val simps_by_f = sort saved_simps
diff -r bdcabcffaaf6 -r e49bfeb0d822 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -469,7 +469,7 @@
     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.generatedK facts |>> map snd end;
+  in lthy |> LocalTheory.notes "" 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;
@@ -880,7 +880,7 @@
       |> 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.generatedK,
+    val flags = {quiet_mode = false, verbose = verbose, kind = "",
       alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
       skip_mono = false, fork_mono = not int};
   in
diff -r bdcabcffaaf6 -r e49bfeb0d822 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -351,7 +351,7 @@
 
     val (ind_info, thy3') = thy2 |>
       Inductive.add_inductive_global (serial ())
-        {quiet_mode = false, verbose = false, kind = Thm.generatedK, alt_name = Binding.empty,
+        {quiet_mode = false, verbose = false, kind = "", alt_name = Binding.empty,
           coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
diff -r bdcabcffaaf6 -r e49bfeb0d822 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -277,10 +277,8 @@
     lthy
     |> set_group ? LocalTheory.set_group (serial ())
     |> add_primrec_simple fixes (map snd spec)
-    |-> (fn (prefix, simps) => fold_map (LocalTheory.note Thm.generatedK)
-          (attr_bindings prefix ~~ simps)
-    #-> (fn simps' => LocalTheory.note Thm.generatedK
-          (simp_attr_binding prefix, maps snd simps')))
+    |-> (fn (prefix, simps) => fold_map (LocalTheory.note "") (attr_bindings prefix ~~ simps)
+      #-> (fn simps' => LocalTheory.note "" (simp_attr_binding prefix, maps snd simps')))
     |>> snd
   end;
 
diff -r bdcabcffaaf6 -r e49bfeb0d822 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -214,8 +214,8 @@
     lthy
     |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     |-> (fn proto_simps => prove_simps proto_simps)
-    |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
-           Code.add_default_eqn_attrib :: map (Attrib.internal o K)
+    |-> (fn simps => LocalTheory.note ""
+      ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K)
           [Simplifier.simp_add, Nitpick_Simps.add]), simps))
     |> snd
   end
diff -r bdcabcffaaf6 -r e49bfeb0d822 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -242,8 +242,7 @@
         ((thm_name, [src]), [thm])
       end;
     val (thmss, lthy'') = lthy'
-      |> fold_map (LocalTheory.note Thm.generatedK)
-        (induct_note :: map unfold_note unfold_thms);
+      |> fold_map (LocalTheory.note "") (induct_note :: map unfold_note unfold_thms);
   in
     (lthy'', names, fixdef_thms, map snd unfold_thms)
   end;
@@ -465,7 +464,7 @@
       val simps2 : (Attrib.binding * thm list) list =
         map (apsnd (fn thm => [thm])) (flat simps);
       val (_, lthy'') = lthy'
-        |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
+        |> fold_map (LocalTheory.note "") (simps1 @ simps2);
     in
       lthy''
     end
diff -r bdcabcffaaf6 -r e49bfeb0d822 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -120,7 +120,7 @@
 
 fun attribute thy = attribute_i thy o intern_src thy;
 
-fun eval_thms ctxt args = ProofContext.note_thmss Thm.generatedK
+fun eval_thms ctxt args = ProofContext.note_thmss ""
     [(Thm.empty_binding, args |> map (fn (a, atts) =>
         (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
   |> fst |> maps snd;
diff -r bdcabcffaaf6 -r e49bfeb0d822 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Nov 13 15:48:52 2009 +0100
+++ b/src/Pure/more_thm.ML	Fri Nov 13 17:25:09 2009 +0100
@@ -86,7 +86,6 @@
   val put_name_hint: string -> thm -> thm
   val definitionK: string
   val theoremK: string
-  val generatedK : string
   val lemmaK: string
   val corollaryK: string
   val get_kind: thm -> string
@@ -413,7 +412,6 @@
 
 val definitionK = "definition";
 val theoremK = "theorem";
-val generatedK = "generatedK"
 val lemmaK = "lemma";
 val corollaryK = "corollary";