1.1 --- a/src/Pure/Thy/thy_header.scala	Fri Jul 20 21:05:47 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Jul 20 22:29:25 2012 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  import scala.util.parsing.input.{Reader, CharSequenceReader}
     1.5  import scala.util.matching.Regex
     1.6  
     1.7 -import java.io.File
     1.8 +import java.io.{File => JFile}
     1.9  
    1.10  
    1.11  object Thy_Header extends Parse.Parser
    1.12 @@ -102,7 +102,7 @@
    1.13    def read(source: CharSequence): Thy_Header =
    1.14      read(new CharSequenceReader(source))
    1.15  
    1.16 -  def read(file: File): Thy_Header =
    1.17 +  def read(file: JFile): Thy_Header =
    1.18    {
    1.19      val reader = Scan.byte_reader(file)
    1.20      try { read(reader).map(Standard_System.decode_permissive_utf8) }