--- a/src/HOL/Nominal/nominal_inductive.ML Fri Nov 13 19:57:46 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Nov 13 20:41:29 2009 +0100
@@ -561,20 +561,19 @@
(strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
else (strong_raw_induct RSN (2, rev_mp),
[ind_case_names, Rule_Cases.consumes 1]);
- val ((_, [strong_induct']), ctxt') = LocalTheory.note ""
+ val ((_, [strong_induct']), ctxt') = ctxt |> LocalTheory.note
((rec_qualified (Binding.name "strong_induct"),
- map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
- ctxt;
+ map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct]);
val strong_inducts =
- Project_Rule.projects ctxt (1 upto length names) strong_induct'
+ Project_Rule.projects ctxt (1 upto length names) strong_induct';
in
ctxt' |>
- LocalTheory.note ""
+ LocalTheory.note
((rec_qualified (Binding.name "strong_inducts"),
[Attrib.internal (K ind_case_names),
Attrib.internal (K (Rule_Cases.consumes 1))]),
strong_inducts) |> snd |>
- LocalTheory.notes "" (map (fn ((name, elim), (_, cases)) =>
+ LocalTheory.notes (map (fn ((name, elim), (_, cases)) =>
((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
[Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
@@ -664,7 +663,7 @@
end) atoms
in
ctxt |>
- LocalTheory.notes "" (map (fn (name, ths) =>
+ LocalTheory.notes (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