diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/PIDE/headless.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -224,7 +224,7 @@
           }
           else result
 
-        val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory(_))
+        val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory)
 
         (load_theories,
           copy(already_committed = already_committed1, result = result1, load_state = load_state1))
@@ -350,7 +350,7 @@
                     (theory_progress, st.update(nodes_status1))
                   })
 
-              theory_progress.foreach(progress.theory(_))
+              theory_progress.foreach(progress.theory)
 
               check_state()
 
@@ -496,7 +496,7 @@
       lazy val theory_graph: Document.Node.Name.Graph[Unit] =
         Document.Node.Name.make_graph(
           for ((name, theory) <- theories.toList)
-          yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_))))
+          yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt)))
 
       def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
 
@@ -542,7 +542,7 @@
         : ((List[Document.Node.Name], List[Document.Node.Name], List[Document.Edit_Text]), State) =
       {
         val all_nodes = theory_graph.topological_order
-        val purge = nodes.getOrElse(all_nodes).filterNot(is_required(_)).toSet
+        val purge = nodes.getOrElse(all_nodes).filterNot(is_required).toSet
 
         val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
         val (retained, purged) = all_nodes.partition(retain)