# HG changeset patch
# User wenzelm
# Date 1568904147 -7200
# Node ID 29243d779b61f015576389103a3098c24cff5846
# Parent  dea35c31a0b852f73e157f0f428c45325195b1dc
unused;

diff -r dea35c31a0b8 -r 29243d779b61 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Sep 19 16:38:32 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Sep 19 16:42:27 2019 +0200
@@ -71,13 +71,6 @@
   sealed case class Known(
     theories: Map[String, Document.Node.Entry] = Map.empty,
     loaded_files: Map[String, List[Path]] = Map.empty)
-  {
-    def platform_path: Known =
-      copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))))
-
-    def standard_path: Known =
-      copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_))))
-  }
 
   object Base
   {