# HG changeset patch
# User wenzelm
# Date 1489572427 -3600
# Node ID d388e63a46fccb335c367497ab1f60a0682433b7
# Parent  3075aa3b40bf3ca97955789cb6c530454b6164c1
unused;

diff -r 3075aa3b40bf -r d388e63a46fc src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Mar 15 11:04:46 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Wed Mar 15 11:07:07 2017 +0100
@@ -13,11 +13,6 @@
 import java.io.{File => JFile}
 
 
-object Resources
-{
-  val empty: Resources = new Resources(Sessions.Base.empty)
-}
-
 class Resources(val base: Sessions.Base, val log: Logger = No_Logger)
 {
   val thy_info = new Thy_Info(this)