diff -r 9a40720750dc -r fa04b549f652 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Sep 03 19:20:22 2019 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Sep 04 11:21:07 2019 +0200
@@ -76,9 +76,11 @@
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[Command.Edit, Command.Perspective]
 
+  type Theory_Graph[A] = Graph[Node.Name, A]
+
   def theory_graph[A](
       entries: List[((Node.Name, A), List[Node.Name])],
-      permissive: Boolean = false): Graph[Node.Name, A] =
+      permissive: Boolean = false): Theory_Graph[A] =
     Graph.make(entries, symmetric = true, permissive = permissive)(Node.Name.Theory_Ordering)
 
   object Node