src/Pure/PIDE/session.scala

   case class Statistics(props: Properties.T)
   case class Global_Options(options: Options)
   case object Caret_Focus
   case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
-  case class Use_Theories(options: Options, id: String, master_dir: Path, thys: List[Path])
+  case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
   sealed abstract class Phase
   case object Inactive extends Phase

 
           case Session.Dialog_Result(id, serial, result) if prover.defined =>
             prover.get.dialog_result(serial, result)
             handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
 
-          case Session.Use_Theories(options, id, master_dir, thys) if prover.defined =>
-            prover.get.use_theories(options, id, master_dir, thys)
+          case Session.Build_Theories(id, master_dir, theories) if prover.defined =>
+            prover.get.build_theories(id, master_dir, theories)
 
           case Protocol_Command(name, args) if prover.defined =>
             prover.get.protocol_command(name, args:_*)
 
           case change: Session.Change if prover.defined =>

   }
 
   def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
   { manager.send(Session.Dialog_Result(id, serial, result)) }
 
-  def use_theories(options: Options, id: String, master_dir: Path, thys: List[Path])
-  { manager.send(Session.Use_Theories(options, id, master_dir, thys)) }
+  def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
+  { manager.send(Session.Build_Theories(id, master_dir, theories)) }
 }