src/Pure/Thy/thy_load.scala
changeset 48409 0d2114eb412a
parent 46938 cda018294515
child 48422 9613780a805b
--- a/src/Pure/Thy/thy_load.scala	Fri Jul 20 21:05:47 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Fri Jul 20 22:29:25 2012 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-import java.io.File
+import java.io.{File => JFile}
 
 
 
@@ -31,7 +31,7 @@
 
   def read_header(name: Document.Node.Name): Thy_Header =
   {
-    val file = new File(name.node)
+    val file = new JFile(name.node)
     if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
     Thy_Header.read(file)
   }