diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -41,7 +41,7 @@
 sig
   val thatN: string
   val obtain: string -> (Name.binding * string option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * (string * string list) list) list ->
+    (Attrib.binding * (string * string list) list) list ->
     bool -> Proof.state -> Proof.state
   val obtain_i: string -> (Name.binding * typ option * mixfix) list ->
     ((Name.binding * attribute list) * (term * term list) list) list ->