src/Pure/Tools/build.scala

             case _: XML.Error => ignore_error("")
           }
       }
     }
 
-    def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue =
+    def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
     {
       val graph = sessions.build_graph
       val names = graph.keys
 
       val timings = names.map(name => (name, load_timings(progress, store, name)))

   /* job: running prover process */
 
   private class Job(progress: Progress,
     name: String,
     val info: Sessions.Info,
-    sessions: Sessions.T,
+    sessions: Sessions.Structure,
     deps: Sessions.Deps,
     store: Sessions.Store,
     do_output: Boolean,
     verbose: Boolean,
     pide: Boolean,