nested source: error msg passed to recover;

--- a/src/Pure/General/source.ML	Mon Jul 09 23:12:38 2007 +0200
+++ b/src/Pure/General/source.ML	Mon Jul 09 23:12:40 2007 +0200
@@ -22,10 +22,10 @@
   val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
   val tty: (string, unit) source
   val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
-    ('a * 'b list -> 'c list * ('a * 'b list)) option ->
+    (string -> 'a * 'b list -> 'c list * ('a * 'b list)) option ->
     ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
   val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
-    ('a list -> 'b list * 'a list) option ->
+    (string -> 'a list -> 'b list * 'a list) option ->
     ('a, 'd) source -> ('b, ('a, 'd) source) source
 end;