# HG changeset patch
# User wenzelm
# Date 1489603174 -3600
# Node ID 2947837b9f0484057e4b01779e15b24299f14251
# Parent  75f2aa8ecb128b76fff2cecdac6e6dab6ddbdc70
unused;

diff -r 75f2aa8ecb12 -r 2947837b9f04 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Mar 15 19:33:34 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Mar 15 19:39:34 2017 +0100
@@ -35,8 +35,6 @@
 
   object Base
   {
-    val empty: Base = Base()
-
     lazy val bootstrap: Base =
       Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
   }
diff -r 75f2aa8ecb12 -r 2947837b9f04 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Mar 15 19:33:34 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Mar 15 19:39:34 2017 +0100
@@ -21,11 +21,6 @@
 import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 
-object JEdit_Resources
-{
-  val empty: JEdit_Resources = new JEdit_Resources(Sessions.Base.empty)
-}
-
 class JEdit_Resources(base: Sessions.Base) extends Resources(base)
 {
   /* document node name */