diff -r a56eab490f4e -r 4c98d37e1448 src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Sun Sep 01 22:57:25 2019 +0200 +++ b/src/Pure/PIDE/headless.scala Mon Sep 02 10:41:14 2019 +0200 @@ -399,7 +399,7 @@ val entries = for ((name, theory) <- theories.toList) yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_))) - Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering) + Graph.make(entries, symmetric = true)(Document.Node.Name.Theory_Ordering) } def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)