src/Pure/PIDE/headless.scala

       {
         require(remove.forall(name => !is_required(name)))
         copy(theories = theories -- remove)
       }
 
-      def unload_theories(session: Session, id: UUID.T, dep_theories: List[Document.Node.Name])
+      def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name])
         : State =
       {
-        val st1 = remove_required(id, dep_theories)
+        val st1 = remove_required(id, theories)
         val theory_edits =
           for {
-            node_name <- dep_theories
+            node_name <- theories
             theory <- st1.theories.get(node_name)
           }
           yield {
             val theory1 = theory.required(st1.is_required(node_name))
             val edits = theory1.node_edits(Some(theory))

     private val state = Synchronized(Resources.State())
 
     def load_theories(
       session: Session,
       id: UUID.T,
-      dep_theories: List[Document.Node.Name],
-      dep_files: List[Document.Node.Name],
+      theories: List[Document.Node.Name],
+      files: List[Document.Node.Name],
       unicode_symbols: Boolean,
       share_common_data: Boolean,
       progress: Progress)
     {
       val loaded_theories =
-        for (node_name <- dep_theories)
+        for (node_name <- theories)
         yield {
           val path = node_name.path
           if (!node_name.is_theory) error("Not a theory file: " + path)
 
           progress.expose_interrupt()

       val loaded = loaded_theories.length
       if (loaded > 1) progress.echo("Loading " + loaded + " theories ...")
 
       state.change(st =>
         {
-          val (doc_blobs1, st1) = st.insert_required(id, dep_theories).update_blobs(dep_files)
+          val (doc_blobs1, st1) = st.insert_required(id, theories).update_blobs(files)
           val theory_edits =
             for (theory <- loaded_theories)
             yield {
               val node_name = theory.node_name
               val theory1 = theory.required(st1.is_required(node_name))
               val edits = theory1.node_edits(st1.theories.get(node_name))
               (edits, (node_name, theory1))
             }
           val file_edits =
-            for { node_name <- dep_files if doc_blobs1.changed(node_name) }
+            for { node_name <- files if doc_blobs1.changed(node_name) }
             yield st1.blob_edits(node_name, st.blobs.get(node_name))
 
           session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten,
             share_common_data = share_common_data)
           st1.update_theories(theory_edits.map(_._2))
         })
     }
 
-    def unload_theories(session: Session, id: UUID.T, dep_theories: List[Document.Node.Name])
-    {
-      state.change(_.unload_theories(session, id, dep_theories))
+    def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name])
+    {
+      state.change(_.unload_theories(session, id, theories))
     }
 
     def clean_theories(session: Session, id: UUID.T, clean: Set[Document.Node.Name])
     {
       state.change(st =>