# HG changeset patch
# User wenzelm
# Date 1184015560 -7200
# Node ID 2d618c190466567f269c61a8afc0018bc033d93e
# Parent  c7cbab93f1d95661c0751560c93c02f897ed1c19
nested source: error msg passed to recover;

diff -r c7cbab93f1d9 -r 2d618c190466 src/Pure/General/source.ML
--- 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;