attribute: Context.mapping;
PureThy.note_thmss_i;

--- a/src/HOL/Tools/inductive_package.ML	Mon Oct 09 02:19:52 2006 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 09 02:19:54 2006 +0200
@@ -128,7 +128,7 @@
 (** monotonicity rules **)
 
 val get_monos = #2 o InductiveData.get;
-val map_monos = Context.map_theory o InductiveData.map o Library.apsnd;
+val map_monos = InductiveData.map o Library.apsnd;
 
 fun mk_mono thm =
   let
@@ -148,8 +148,11 @@
 
 (* attributes *)
 
-val mono_add = Thm.declaration_attribute (map_monos o fold Drule.add_rule o mk_mono);
-val mono_del = Thm.declaration_attribute (map_monos o fold Drule.del_rule o mk_mono);
+val mono_add = Thm.declaration_attribute (fn th =>
+  Context.mapping (map_monos (fold Drule.add_rule (mk_mono th))) I);
+
+val mono_del = Thm.declaration_attribute (fn th =>
+  Context.mapping (map_monos (fold Drule.del_rule (mk_mono th))) I);
 
 
 
@@ -572,7 +575,7 @@
 
     val facts = args |> map (fn ((a, atts), props) =>
      ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
-  in thy |> IsarThy.theorems_i PureThy.lemmaK facts |> snd end;
+  in thy |> PureThy.note_thmss_i "" facts |> snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.attribute ProofContext.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;