# HG changeset patch
# User wenzelm
# Date 1670927126 -3600
# Node ID 95c258c0753cbe443021ee140cc4bab94aa67a5b
# Parent  2447d947d90000bebd21140e6c26a894fb25de29
clarified order: accumulate strictly from left to right;

diff -r 2447d947d900 -r 95c258c0753c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Dec 13 11:18:27 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Dec 13 11:25:26 2022 +0100
@@ -1176,8 +1176,8 @@
         case None =>
           seen_roots += (root.key -> (root, next_root))
           next_root += 1
-        case Some((root1, next1)) =>
-          seen_roots += (root.key -> (root || root1, next1))
+        case Some((root0, next0)) =>
+          seen_roots += (root0.key -> (root0 || root, next0))
       }
     }
     seen_roots.valuesIterator.toList.sortBy(_._2).map(_._1)