# HG changeset patch
# User haftmann
# Date 1242632977 -7200
# Node ID 80b7adb23866646f18f47628d180c859a58f9df7
# Parent  c39994cb152ab8c0d0aaa000f77e5456ec7295dd# Parent  7d43c7d3a15cd41e98bf17532d21db47c13bfa55
merged

diff -r 7d43c7d3a15c -r 80b7adb23866 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Mon May 18 09:49:37 2009 +0200
@@ -561,7 +561,7 @@
             (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
           else (strong_raw_induct RSN (2, rev_mp),
             [ind_case_names, RuleCases.consumes 1]);
-        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generated_theoremK
+        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
           ((rec_qualified (Binding.name "strong_induct"),
             map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
           ctxt;
@@ -569,12 +569,12 @@
           ProjectRule.projects ctxt (1 upto length names) strong_induct'
       in
         ctxt' |>
-        LocalTheory.note Thm.generated_theoremK
+        LocalTheory.note Thm.generatedK
           ((rec_qualified (Binding.name "strong_inducts"),
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (RuleCases.consumes 1))]),
            strong_inducts) |> snd |>
-        LocalTheory.notes Thm.generated_theoremK (map (fn ((name, elim), (_, cases)) =>
+        LocalTheory.notes Thm.generatedK (map (fn ((name, elim), (_, cases)) =>
             ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
               [Attrib.internal (K (RuleCases.case_names (map snd cases))),
                Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
@@ -664,7 +664,7 @@
       end) atoms
   in
     ctxt |>
-    LocalTheory.notes Thm.generated_theoremK (map (fn (name, ths) =>
+    LocalTheory.notes Thm.generatedK (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 7d43c7d3a15c -r 80b7adb23866 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon May 18 09:49:37 2009 +0200
@@ -461,7 +461,7 @@
             (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
           else (strong_raw_induct RSN (2, rev_mp),
             [ind_case_names, RuleCases.consumes 1]);
-        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generated_theoremK
+        val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
           ((rec_qualified (Binding.name "strong_induct"),
             map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
           ctxt;
@@ -469,7 +469,7 @@
           ProjectRule.projects ctxt' (1 upto length names) strong_induct'
       in
         ctxt' |>
-        LocalTheory.note Thm.generated_theoremK
+        LocalTheory.note Thm.generatedK
           ((rec_qualified (Binding.name "strong_inducts"),
             [Attrib.internal (K ind_case_names),
              Attrib.internal (K (RuleCases.consumes 1))]),
diff -r 7d43c7d3a15c -r 80b7adb23866 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Mon May 18 09:49:37 2009 +0200
@@ -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.generated_theoremK)
+           val (simps', lthy'') = fold_map (LocalTheory.note Thm.generatedK)
              (names_atts' ~~ map single simps) lthy'
          in
            lthy''
-           |> LocalTheory.note Thm.generated_theoremK ((qualify (Binding.name "simps"),
+           |> LocalTheory.note Thm.generatedK ((qualify (Binding.name "simps"),
                 map (Attrib.internal o K)
                     [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
                 maps snd simps')
diff -r 7d43c7d3a15c -r 80b7adb23866 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon May 18 09:49:37 2009 +0200
@@ -45,7 +45,7 @@
      Nitpick_Const_Psimp_Thms.add]
 
 fun note_theorem ((name, atts), ths) =
-  LocalTheory.note Thm.generated_theoremK ((Binding.qualified_name name, atts), ths)
+  LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 
@@ -56,7 +56,7 @@
                    |> map (apfst (apfst extra_qualify))
 
       val (saved_spec_simps, lthy) =
-        fold_map (LocalTheory.note Thm.generated_theoremK) spec lthy
+        fold_map (LocalTheory.note Thm.generatedK) spec lthy
 
       val saved_simps = flat (map snd saved_spec_simps)
       val simps_by_f = sort saved_simps
diff -r 7d43c7d3a15c -r 80b7adb23866 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon May 18 09:49:37 2009 +0200
@@ -454,7 +454,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.generated_theoremK facts |>> map snd end;
+  in lthy |> LocalTheory.notes Thm.generatedK 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;
@@ -849,7 +849,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.generated_theoremK,
+    val flags = {quiet_mode = false, verbose = verbose, kind = Thm.generatedK,
       alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
       skip_mono = false, fork_mono = not int};
   in
diff -r 7d43c7d3a15c -r 80b7adb23866 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon May 18 09:49:37 2009 +0200
@@ -349,7 +349,7 @@
 
     val (ind_info, thy3') = thy2 |>
       InductivePackage.add_inductive_global (serial_string ())
-        {quiet_mode = false, verbose = false, kind = Thm.generated_theoremK, alt_name = Binding.empty,
+        {quiet_mode = false, verbose = false, kind = Thm.generatedK, 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 7d43c7d3a15c -r 80b7adb23866 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Mon May 18 09:49:37 2009 +0200
@@ -253,8 +253,8 @@
     |> set_group ? LocalTheory.set_group (serial_string ())
     |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
     |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
-    |-> (fn simps => fold_map (LocalTheory.note Thm.generated_theoremK) simps)
-    |-> (fn simps' => LocalTheory.note Thm.generated_theoremK
+    |-> (fn simps => fold_map (LocalTheory.note Thm.generatedK) simps)
+    |-> (fn simps' => LocalTheory.note Thm.generatedK
           ((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps'))
     |>> snd
   end handle PrimrecError (msg, some_eqn) =>
diff -r 7d43c7d3a15c -r 80b7adb23866 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Mon May 18 09:49:37 2009 +0200
@@ -1393,7 +1393,7 @@
     val (predname, _) = dest_Const pred
     fun after_qed [[th]] lthy'' =
       lthy''
-      |> LocalTheory.note Thm.generated_theoremK
+      |> LocalTheory.note Thm.generatedK
            ((Binding.empty, [Attrib.internal (K add_elim_attrib)]), [th])
       |> snd
       |> LocalTheory.theory (prove_equation predname NONE)
diff -r 7d43c7d3a15c -r 80b7adb23866 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Mon May 18 09:49:37 2009 +0200
@@ -195,7 +195,7 @@
     val unfold_thms = unfolds names tuple_unfold_thm;
     fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
     val (thmss, lthy'') = lthy'
-      |> fold_map (LocalTheory.note Thm.generated_theoremK o mk_note)
+      |> fold_map (LocalTheory.note Thm.generatedK o mk_note)
         ((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
   in
     (lthy'', names, fixdef_thms, map snd unfold_thms)
@@ -373,7 +373,7 @@
       val simps2 : (Attrib.binding * thm list) list =
         map (apsnd (fn thm => [thm])) (List.concat simps);
       val (_, lthy'') = lthy'
-        |> fold_map (LocalTheory.note Thm.generated_theoremK) (simps1 @ simps2);
+        |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
     in
       lthy''
     end
diff -r 7d43c7d3a15c -r 80b7adb23866 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon May 18 09:49:37 2009 +0200
@@ -123,7 +123,7 @@
 
 fun attribute thy = attribute_i thy o intern_src thy;
 
-fun eval_thms ctxt args = ProofContext.note_thmss Thm.generated_theoremK
+fun eval_thms ctxt args = ProofContext.note_thmss Thm.generatedK
     [(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 7d43c7d3a15c -r 80b7adb23866 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Mon May 18 09:49:37 2009 +0200
@@ -66,7 +66,7 @@
       case Thm.get_group thm of
         NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
     val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
-      if member (op =) [Thm.theoremK, Thm.generated_theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
+      if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
         andalso is_unused p
       then
         (case Thm.get_group thm of
diff -r 7d43c7d3a15c -r 80b7adb23866 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon May 18 09:47:34 2009 +0200
+++ b/src/Pure/more_thm.ML	Mon May 18 09:49:37 2009 +0200
@@ -70,7 +70,7 @@
   val assumptionK: string
   val definitionK: string
   val theoremK: string
-  val generated_theoremK : string
+  val generatedK : string
   val lemmaK: string
   val corollaryK: string
   val internalK: string
@@ -389,7 +389,7 @@
 val assumptionK = "assumption";
 val definitionK = "definition";
 val theoremK = "theorem";
-val generated_theoremK = "generated_theoremK"
+val generatedK = "generatedK"
 val lemmaK = "lemma";
 val corollaryK = "corollary";
 val internalK = Markup.internalK;