src/Pure/pure_thy.ML

   val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
   val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
     -> theory -> (string * thm list) list * theory
-  val note_thmss_grouped: string -> string -> (Thm.binding * (thm list * attribute list) list) list
-    -> theory -> (string * thm list) list * theory
   val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
   val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
   val add_defs: bool -> ((binding * term) * attribute list) list ->
     theory -> thm list * theory
   val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->

       (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
 
 
 (* note_thmss *)
 
-local
-
-fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
+fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
   let
     val pos = Binding.pos_of b;
     val name = Sign.full_name thy b;
     val _ = Position.report (Markup.fact_decl name) pos;
 
     fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
     val (thms, thy') = thy |> enter_thms
       (name_thmss true pos) (name_thms false true pos) (apsnd flat o Library.foldl_map app)
-      (b, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts);
+      (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts);
   in ((name, thms), thy') end);
-
-in
-
-fun note_thmss k = gen_note_thmss (Thm.kind k);
-fun note_thmss_grouped k g = gen_note_thmss (Thm.kind k #> Thm.group g);
-
-end;
 
 
 (* store axioms as theorems *)
 
 local