src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -12,7 +12,7 @@
 import scala.util.parsing.input.{Reader, CharSequenceReader}
 import scala.util.matching.Regex
 
-import java.io.File
+import java.io.{File => JFile}
 
 
 object Thy_Header extends Parse.Parser
@@ -102,7 +102,7 @@
   def read(source: CharSequence): Thy_Header =
     read(new CharSequenceReader(source))
 
-  def read(file: File): Thy_Header =
+  def read(file: JFile): Thy_Header =
   {
     val reader = Scan.byte_reader(file)
     try { read(reader).map(Standard_System.decode_permissive_utf8) }