# HG changeset patch
# User wenzelm
# Date 1238676590 -7200
# Node ID 6c6b7a72fa3451092bc264561db20788f2bfdf34
# Parent  59a422908e2933ab7ed26939b01983d15cbcab5f
tuned signature;

diff -r 59a422908e29 -r 6c6b7a72fa34 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Apr 02 14:30:16 2009 +0200
+++ b/src/Pure/pure_thy.ML	Thu Apr 02 14:49:50 2009 +0200
@@ -31,10 +31,10 @@
   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 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 ->