introduced Thm.generatedK
authorhaftmann
Mon May 18 09:48:06 2009 +0200 (2009-05-18)
changeset 31177c39994cb152a
parent 31176 92e0ed53db25
child 31190 80b7adb23866
child 31197 c1c163ec6c44
child 31199 10d413b08fa7
introduced Thm.generatedK
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/primrec_package.ML
src/HOL/ex/predicate_compile.ML
src/HOLCF/Tools/fixrec_package.ML
src/Pure/Isar/attrib.ML
src/Pure/Thy/thm_deps.ML
src/Pure/more_thm.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sun May 17 07:17:39 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon May 18 09:48:06 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.generated_theoremK
     1.8 +        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
     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.generated_theoremK
    1.17 +        LocalTheory.note Thm.generatedK
    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.generated_theoremK (map (fn ((name, elim), (_, cases)) =>
    1.23 +        LocalTheory.notes Thm.generatedK (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.generated_theoremK (map (fn (name, ths) =>
    1.32 +    LocalTheory.notes Thm.generatedK (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	Sun May 17 07:17:39 2009 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon May 18 09:48:06 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.generated_theoremK
     2.8 +        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
     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.generated_theoremK
    2.17 +        LocalTheory.note Thm.generatedK
    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	Sun May 17 07:17:39 2009 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Mon May 18 09:48:06 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.generated_theoremK)
     3.8 +           val (simps', lthy'') = fold_map (LocalTheory.note Thm.generatedK)
     3.9               (names_atts' ~~ map single simps) lthy'
    3.10           in
    3.11             lthy''
    3.12 -           |> LocalTheory.note Thm.generated_theoremK ((qualify (Binding.name "simps"),
    3.13 +           |> LocalTheory.note Thm.generatedK ((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/Tools/function_package/fundef_package.ML	Sun May 17 07:17:39 2009 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon May 18 09:48:06 2009 +0200
     4.3 @@ -45,7 +45,7 @@
     4.4       Nitpick_Const_Psimp_Thms.add]
     4.5  
     4.6  fun note_theorem ((name, atts), ths) =
     4.7 -  LocalTheory.note Thm.generated_theoremK ((Binding.qualified_name name, atts), ths)
     4.8 +  LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
     4.9  
    4.10  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
    4.11  
    4.12 @@ -56,7 +56,7 @@
    4.13                     |> map (apfst (apfst extra_qualify))
    4.14  
    4.15        val (saved_spec_simps, lthy) =
    4.16 -        fold_map (LocalTheory.note Thm.generated_theoremK) spec lthy
    4.17 +        fold_map (LocalTheory.note Thm.generatedK) spec lthy
    4.18  
    4.19        val saved_simps = flat (map snd saved_spec_simps)
    4.20        val simps_by_f = sort saved_simps
     5.1 --- a/src/HOL/Tools/inductive_package.ML	Sun May 17 07:17:39 2009 +0200
     5.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon May 18 09:48:06 2009 +0200
     5.3 @@ -454,7 +454,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.generated_theoremK facts |>> map snd end;
     5.8 +  in lthy |> LocalTheory.notes Thm.generatedK 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 @@ -849,7 +849,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.generated_theoremK,
    5.17 +    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.generatedK,
    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	Sun May 17 07:17:39 2009 +0200
     6.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon May 18 09:48:06 2009 +0200
     6.3 @@ -349,7 +349,7 @@
     6.4  
     6.5      val (ind_info, thy3') = thy2 |>
     6.6        InductivePackage.add_inductive_global (serial_string ())
     6.7 -        {quiet_mode = false, verbose = false, kind = Thm.generated_theoremK, alt_name = Binding.empty,
     6.8 +        {quiet_mode = false, verbose = false, kind = Thm.generatedK, 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_package.ML	Sun May 17 07:17:39 2009 +0200
     7.2 +++ b/src/HOL/Tools/primrec_package.ML	Mon May 18 09:48:06 2009 +0200
     7.3 @@ -253,8 +253,8 @@
     7.4      |> set_group ? LocalTheory.set_group (serial_string ())
     7.5      |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
     7.6      |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
     7.7 -    |-> (fn simps => fold_map (LocalTheory.note Thm.generated_theoremK) simps)
     7.8 -    |-> (fn simps' => LocalTheory.note Thm.generated_theoremK
     7.9 +    |-> (fn simps => fold_map (LocalTheory.note Thm.generatedK) simps)
    7.10 +    |-> (fn simps' => LocalTheory.note Thm.generatedK
    7.11            ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps'))
    7.12      |>> snd
    7.13    end handle PrimrecError (msg, some_eqn) =>
     8.1 --- a/src/HOL/ex/predicate_compile.ML	Sun May 17 07:17:39 2009 +0200
     8.2 +++ b/src/HOL/ex/predicate_compile.ML	Mon May 18 09:48:06 2009 +0200
     8.3 @@ -1393,7 +1393,7 @@
     8.4      val (predname, _) = dest_Const pred
     8.5      fun after_qed [[th]] lthy'' =
     8.6        lthy''
     8.7 -      |> LocalTheory.note Thm.generated_theoremK
     8.8 +      |> LocalTheory.note Thm.generatedK
     8.9             ((Binding.empty, [Attrib.internal (K add_elim_attrib)]), [th])
    8.10        |> snd
    8.11        |> LocalTheory.theory (prove_equation predname NONE)
     9.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Sun May 17 07:17:39 2009 +0200
     9.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Mon May 18 09:48:06 2009 +0200
     9.3 @@ -195,7 +195,7 @@
     9.4      val unfold_thms = unfolds names tuple_unfold_thm;
     9.5      fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
     9.6      val (thmss, lthy'') = lthy'
     9.7 -      |> fold_map (LocalTheory.note Thm.generated_theoremK o mk_note)
     9.8 +      |> fold_map (LocalTheory.note Thm.generatedK o mk_note)
     9.9          ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
    9.10    in
    9.11      (lthy'', names, fixdef_thms, map snd unfold_thms)
    9.12 @@ -373,7 +373,7 @@
    9.13        val simps2 : (Attrib.binding * thm list) list =
    9.14          map (apsnd (fn thm => [thm])) (List.concat simps);
    9.15        val (_, lthy'') = lthy'
    9.16 -        |> fold_map (LocalTheory.note Thm.generated_theoremK) (simps1 @ simps2);
    9.17 +        |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
    9.18      in
    9.19        lthy''
    9.20      end
    10.1 --- a/src/Pure/Isar/attrib.ML	Sun May 17 07:17:39 2009 +0200
    10.2 +++ b/src/Pure/Isar/attrib.ML	Mon May 18 09:48:06 2009 +0200
    10.3 @@ -123,7 +123,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.generated_theoremK
    10.8 +fun eval_thms ctxt args = ProofContext.note_thmss Thm.generatedK
    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/Thy/thm_deps.ML	Sun May 17 07:17:39 2009 +0200
    11.2 +++ b/src/Pure/Thy/thm_deps.ML	Mon May 18 09:48:06 2009 +0200
    11.3 @@ -66,7 +66,7 @@
    11.4        case Thm.get_group thm of
    11.5          NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
    11.6      val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
    11.7 -      if member (op =) [Thm.theoremK, Thm.generated_theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
    11.8 +      if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
    11.9          andalso is_unused p
   11.10        then
   11.11          (case Thm.get_group thm of
    12.1 --- a/src/Pure/more_thm.ML	Sun May 17 07:17:39 2009 +0200
    12.2 +++ b/src/Pure/more_thm.ML	Mon May 18 09:48:06 2009 +0200
    12.3 @@ -70,7 +70,7 @@
    12.4    val assumptionK: string
    12.5    val definitionK: string
    12.6    val theoremK: string
    12.7 -  val generated_theoremK : string
    12.8 +  val generatedK : string
    12.9    val lemmaK: string
   12.10    val corollaryK: string
   12.11    val internalK: string
   12.12 @@ -389,7 +389,7 @@
   12.13  val assumptionK = "assumption";
   12.14  val definitionK = "definition";
   12.15  val theoremK = "theorem";
   12.16 -val generated_theoremK = "generated_theoremK"
   12.17 +val generatedK = "generatedK"
   12.18  val lemmaK = "lemma";
   12.19  val corollaryK = "corollary";
   12.20  val internalK = Markup.internalK;