src/Pure/Thy/sessions.scala

--- a/src/Pure/Thy/sessions.scala	Wed Dec 09 15:53:45 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Dec 09 20:10:10 2020 +0100
@@ -635,6 +635,8 @@
 
   object Structure
   {
+    val empty: Structure = make(Nil)
+
     def make(infos: List[Info]): Structure =
     {
       def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])