--- a/src/HOL/Nominal/nominal_inductive.ML Sun May 17 07:17:39 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon May 18 09:48:06 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