unused;

--- 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)
   }

--- 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 */