src/Pure/Thy/thy_info.scala

--- a/src/Pure/Thy/thy_info.scala	Fri Aug 12 11:41:26 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Fri Aug 12 12:03:17 2011 +0200
@@ -38,7 +38,7 @@
 
   /* dependencies */
 
-  type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
+  type Deps = Map[String, Exn.Result[(String, Thy_Header)]]  // name -> (text, header)
 
   private def require_thys(ignored: String => Boolean,
       initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =