eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
authorwenzelm
Fri Nov 13 17:25:09 2009 +0100 (2009-11-13 ago)
changeset 33666e49bfeb0d822
parent 33665 bdcabcffaaf6
child 33668 090288424d44
eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOLCF/Tools/fixrec.ML
src/Pure/Isar/attrib.ML
src/Pure/more_thm.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 15:48:52 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 13 17:25:09 2009 +0100
     1.3 @@ -561,7 +561,7 @@
     1.4              (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
     1.5            else (strong_raw_induct RSN (2, rev_mp),
     1.6              [ind_case_names, Rule_Cases.consumes 1]);
     1.7 -        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
     1.8 +        val ((_, [strong_induct']), ctxt') = LocalTheory.note ""
     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            Project_Rule.projects ctxt (1 upto length names) strong_induct'
    1.14        in
    1.15          ctxt' |>
    1.16 -        LocalTheory.note Thm.generatedK
    1.17 +        LocalTheory.note ""
    1.18            ((rec_qualified (Binding.name "strong_inducts"),
    1.19              [Attrib.internal (K ind_case_names),
    1.20               Attrib.internal (K (Rule_Cases.consumes 1))]),
    1.21             strong_inducts) |> snd |>
    1.22 -        LocalTheory.notes Thm.generatedK (map (fn ((name, elim), (_, cases)) =>
    1.23 +        LocalTheory.notes "" (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 (Rule_Cases.case_names (map snd cases))),
    1.26                 Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
    1.27 @@ -664,7 +664,7 @@
    1.28        end) atoms
    1.29    in
    1.30      ctxt |>
    1.31 -    LocalTheory.notes Thm.generatedK (map (fn (name, ths) =>
    1.32 +    LocalTheory.notes "" (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	Fri Nov 13 15:48:52 2009 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 13 17:25:09 2009 +0100
     2.3 @@ -466,7 +466,7 @@
     2.4              NONE => (rec_qualified (Binding.name "strong_induct"),
     2.5                       rec_qualified (Binding.name "strong_inducts"))
     2.6            | SOME s => (Binding.name s, Binding.name (s ^ "s"));
     2.7 -        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
     2.8 +        val ((_, [strong_induct']), ctxt') = LocalTheory.note ""
     2.9            ((induct_name,
    2.10              map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
    2.11            ctxt;
    2.12 @@ -474,7 +474,7 @@
    2.13            Project_Rule.projects ctxt' (1 upto length names) strong_induct'
    2.14        in
    2.15          ctxt' |>
    2.16 -        LocalTheory.note Thm.generatedK
    2.17 +        LocalTheory.note ""
    2.18            ((inducts_name,
    2.19              [Attrib.internal (K ind_case_names),
    2.20               Attrib.internal (K (Rule_Cases.consumes 1))]),
     3.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 15:48:52 2009 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Nov 13 17:25:09 2009 +0100
     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.generatedK)
     3.8 +           val (simps', lthy'') = fold_map (LocalTheory.note "")
     3.9               (names_atts' ~~ map single simps) lthy'
    3.10           in
    3.11             lthy''
    3.12 -           |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
    3.13 +           |> LocalTheory.note "" ((qualify (Binding.name "simps"),
    3.14                  map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]),
    3.15                  maps snd simps')
    3.16             |> snd
     4.1 --- a/src/HOL/Tools/Function/function.ML	Fri Nov 13 15:48:52 2009 +0100
     4.2 +++ b/src/HOL/Tools/Function/function.ML	Fri Nov 13 17:25:09 2009 +0100
     4.3 @@ -44,7 +44,7 @@
     4.4       Nitpick_Psimps.add]
     4.5  
     4.6  fun note_theorem ((binding, atts), ths) =
     4.7 -  LocalTheory.note Thm.generatedK ((binding, atts), ths)
     4.8 +  LocalTheory.note "" ((binding, atts), ths)
     4.9  
    4.10  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
    4.11  
    4.12 @@ -55,7 +55,7 @@
    4.13                     |> map (apfst (apfst extra_qualify))
    4.14  
    4.15        val (saved_spec_simps, lthy) =
    4.16 -        fold_map (LocalTheory.note Thm.generatedK) spec lthy
    4.17 +        fold_map (LocalTheory.note "") spec lthy
    4.18  
    4.19        val saved_simps = maps snd saved_spec_simps
    4.20        val simps_by_f = sort saved_simps
     5.1 --- a/src/HOL/Tools/inductive.ML	Fri Nov 13 15:48:52 2009 +0100
     5.2 +++ b/src/HOL/Tools/inductive.ML	Fri Nov 13 17:25:09 2009 +0100
     5.3 @@ -469,7 +469,7 @@
     5.4      val facts = args |> map (fn ((a, atts), props) =>
     5.5        ((a, map (prep_att thy) atts),
     5.6          map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
     5.7 -  in lthy |> LocalTheory.notes Thm.generatedK facts |>> map snd end;
     5.8 +  in lthy |> LocalTheory.notes "" facts |>> map snd end;
     5.9  
    5.10  val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
    5.11  val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
    5.12 @@ -880,7 +880,7 @@
    5.13        |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
    5.14      val (cs, ps) = chop (length cnames_syn) vars;
    5.15      val monos = Attrib.eval_thms lthy raw_monos;
    5.16 -    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.generatedK,
    5.17 +    val flags = {quiet_mode = false, verbose = verbose, kind = "",
    5.18        alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
    5.19        skip_mono = false, fork_mono = not int};
    5.20    in
     6.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 15:48:52 2009 +0100
     6.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 17:25:09 2009 +0100
     6.3 @@ -351,7 +351,7 @@
     6.4  
     6.5      val (ind_info, thy3') = thy2 |>
     6.6        Inductive.add_inductive_global (serial ())
     6.7 -        {quiet_mode = false, verbose = false, kind = Thm.generatedK, alt_name = Binding.empty,
     6.8 +        {quiet_mode = false, verbose = false, kind = "", alt_name = Binding.empty,
     6.9            coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
    6.10          rlzpreds rlzparams (map (fn (rintr, intr) =>
    6.11            ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
     7.1 --- a/src/HOL/Tools/primrec.ML	Fri Nov 13 15:48:52 2009 +0100
     7.2 +++ b/src/HOL/Tools/primrec.ML	Fri Nov 13 17:25:09 2009 +0100
     7.3 @@ -277,10 +277,8 @@
     7.4      lthy
     7.5      |> set_group ? LocalTheory.set_group (serial ())
     7.6      |> add_primrec_simple fixes (map snd spec)
     7.7 -    |-> (fn (prefix, simps) => fold_map (LocalTheory.note Thm.generatedK)
     7.8 -          (attr_bindings prefix ~~ simps)
     7.9 -    #-> (fn simps' => LocalTheory.note Thm.generatedK
    7.10 -          (simp_attr_binding prefix, maps snd simps')))
    7.11 +    |-> (fn (prefix, simps) => fold_map (LocalTheory.note "") (attr_bindings prefix ~~ simps)
    7.12 +      #-> (fn simps' => LocalTheory.note "" (simp_attr_binding prefix, maps snd simps')))
    7.13      |>> snd
    7.14    end;
    7.15  
     8.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 15:48:52 2009 +0100
     8.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Nov 13 17:25:09 2009 +0100
     8.3 @@ -214,8 +214,8 @@
     8.4      lthy
     8.5      |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     8.6      |-> (fn proto_simps => prove_simps proto_simps)
     8.7 -    |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
     8.8 -           Code.add_default_eqn_attrib :: map (Attrib.internal o K)
     8.9 +    |-> (fn simps => LocalTheory.note ""
    8.10 +      ((b, Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    8.11            [Simplifier.simp_add, Nitpick_Simps.add]), simps))
    8.12      |> snd
    8.13    end
     9.1 --- a/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 15:48:52 2009 +0100
     9.2 +++ b/src/HOLCF/Tools/fixrec.ML	Fri Nov 13 17:25:09 2009 +0100
     9.3 @@ -242,8 +242,7 @@
     9.4          ((thm_name, [src]), [thm])
     9.5        end;
     9.6      val (thmss, lthy'') = lthy'
     9.7 -      |> fold_map (LocalTheory.note Thm.generatedK)
     9.8 -        (induct_note :: map unfold_note unfold_thms);
     9.9 +      |> fold_map (LocalTheory.note "") (induct_note :: map unfold_note unfold_thms);
    9.10    in
    9.11      (lthy'', names, fixdef_thms, map snd unfold_thms)
    9.12    end;
    9.13 @@ -465,7 +464,7 @@
    9.14        val simps2 : (Attrib.binding * thm list) list =
    9.15          map (apsnd (fn thm => [thm])) (flat simps);
    9.16        val (_, lthy'') = lthy'
    9.17 -        |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
    9.18 +        |> fold_map (LocalTheory.note "") (simps1 @ simps2);
    9.19      in
    9.20        lthy''
    9.21      end
    10.1 --- a/src/Pure/Isar/attrib.ML	Fri Nov 13 15:48:52 2009 +0100
    10.2 +++ b/src/Pure/Isar/attrib.ML	Fri Nov 13 17:25:09 2009 +0100
    10.3 @@ -120,7 +120,7 @@
    10.4  
    10.5  fun attribute thy = attribute_i thy o intern_src thy;
    10.6  
    10.7 -fun eval_thms ctxt args = ProofContext.note_thmss Thm.generatedK
    10.8 +fun eval_thms ctxt args = ProofContext.note_thmss ""
    10.9      [(Thm.empty_binding, args |> map (fn (a, atts) =>
   10.10          (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
   10.11    |> fst |> maps snd;
    11.1 --- a/src/Pure/more_thm.ML	Fri Nov 13 15:48:52 2009 +0100
    11.2 +++ b/src/Pure/more_thm.ML	Fri Nov 13 17:25:09 2009 +0100
    11.3 @@ -86,7 +86,6 @@
    11.4    val put_name_hint: string -> thm -> thm
    11.5    val definitionK: string
    11.6    val theoremK: string
    11.7 -  val generatedK : string
    11.8    val lemmaK: string
    11.9    val corollaryK: string
   11.10    val get_kind: thm -> string
   11.11 @@ -413,7 +412,6 @@
   11.12  
   11.13  val definitionK = "definition";
   11.14  val theoremK = "theorem";
   11.15 -val generatedK = "generatedK"
   11.16  val lemmaK = "lemma";
   11.17  val corollaryK = "corollary";
   11.18