--- 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
--- 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))]),
--- 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')
--- 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
--- 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
--- 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)), []),
--- 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) =>
--- 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)
--- 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
--- 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;
--- 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
--- 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;