added source: string -> (string, string list) Source.source;

--- a/src/Pure/Thy/file.ML	Tue May 19 17:14:01 1998 +0200
+++ b/src/Pure/Thy/file.ML	Tue May 19 17:14:28 1998 +0200
@@ -14,6 +14,7 @@
   val write: string -> string -> unit
   val append: string -> string -> unit
   val copy: string -> string -> unit
+  val source: string -> (string, string list) Source.source
 end;
 
 structure File: FILE =
@@ -60,5 +61,7 @@
   if not (exists infile) then error ("File not found: " ^ quote infile)
   else write outfile (read infile);
 
+val source = Source.of_string o read;
+
 
 end;