author | wenzelm |
Mon, 02 Sep 2019 16:28:09 +0200 | |
changeset 70639 | ad7891a73230 |
parent 70638 | f164cec7ac22 |
child 70640 | 5f4b8a505090 |
--- 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) }