diff -r 78aa7846e91f -r d8a0e996614b src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -48,12 +48,16 @@
         }))
 
     val graph0 =
-      (Graph.string[Option[Theory]] /: thys) {
-        case (g, thy) => g.default_node(thy.name, Some(thy)) }
+      thys.foldLeft(Graph.string[Option[Theory]]) {
+        case (g, thy) => g.default_node(thy.name, Some(thy))
+      }
     val graph1 =
-      (graph0 /: thys) { case (g0, thy) =>
-        (g0 /: thy.parents) { case (g1, parent) =>
-          g1.default_node(parent, None).add_edge_acyclic(parent, thy.name) } }
+      thys.foldLeft(graph0) {
+        case (g0, thy) =>
+          thy.parents.foldLeft(g0) {
+            case (g1, parent) => g1.default_node(parent, None).add_edge_acyclic(parent, thy.name)
+          }
+      }
 
     Session(session_name, graph1)
   }