diff -r e397f6800c3c -r 5542716503ab src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Feb 02 16:31:32 2006 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Feb 02 16:31:33 2006 +0100
@@ -20,11 +20,11 @@
   val intern_src: theory -> src -> src
   val attribute: theory -> src -> attribute
   val attribute_i: theory -> src -> attribute
-  val map_specs: ('a -> attribute) ->
-    (('c * 'a list) * 'd) list -> (('c * attribute list) * 'd) list
-  val map_facts: ('a -> attribute) ->
+  val map_specs: ('a -> 'att) ->
+    (('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list
+  val map_facts: ('a -> 'att) ->
     (('c * 'a list) * ('d * 'a list) list) list ->
-    (('c * attribute list) * ('d * attribute list) list) list
+    (('c * 'att list) * ('d * 'att list) list) list
   val crude_closure: Context.proof -> src -> src
   val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
   val global_thm: theory * Args.T list -> thm * (theory * Args.T list)