--- 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;