# HG changeset patch
# User wenzelm
# Date 1567434489 -7200
# Node ID ad7891a7323038d5ba946236c05acc02480aad32
# Parent  f164cec7ac22c21c4e0733db1faba2d3f69c2cf2
proper orientation;

diff -r f164cec7ac22 -r ad7891a73230 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Sep 02 11:46:27 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Sep 02 16:28:09 2019 +0200
@@ -233,7 +233,7 @@
             else true
           }
         } yield entry
-      Graph.make[Document.Node.Name, Options](used, permissive = true)(
+      Graph.make[Document.Node.Name, Options](used, symmetric = true, permissive = true)(
         Document.Node.Name.Theory_Ordering)
     }