1.1 --- a/src/Pure/pure_thy.ML	Thu Apr 02 14:30:16 2009 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Thu Apr 02 14:49:50 2009 +0200
     1.3 @@ -31,10 +31,10 @@
     1.4    val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
     1.5    val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
     1.6    val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
     1.7 -  val note_thmss: string -> (Thm.binding *
     1.8 -      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
     1.9 -  val note_thmss_grouped: string -> string -> (Thm.binding *
    1.10 -      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
    1.11 +  val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
    1.12 +    -> theory -> (string * thm list) list * theory
    1.13 +  val note_thmss_grouped: string -> string -> (Thm.binding * (thm list * attribute list) list) list
    1.14 +    -> theory -> (string * thm list) list * theory
    1.15    val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
    1.16    val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
    1.17    val add_defs: bool -> ((binding * term) * attribute list) list ->