src/Pure/Thy/sessions.scala
changeset 70876 9cde8c4ea5a5
parent 70875 c1597167563e
child 70877 086575316fd5
--- a/src/Pure/Thy/sessions.scala	Thu Sep 12 13:39:04 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Sep 12 14:22:47 2019 +0200
@@ -182,8 +182,7 @@
       imports getOrElse Base.bootstrap(session_directories, global_theories)
   }
 
-  sealed case class Deps(
-    sessions_structure: Structure, session_bases: Map[String, Base], all_known: Known)
+  sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base])
   {
     override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
 
@@ -429,10 +428,7 @@
           }
       })
 
-    val all_known =
-      Known.make(Path.current, sessions_structure.imports_topological_order.map(session_bases(_)))
-
-    Deps(sessions_structure, session_bases, all_known)
+    Deps(sessions_structure, session_bases)
   }