# HG changeset patch
# User wenzelm
# Date 1483990260 -3600
# Node ID 8fcc23e8e1d974390e33b482e3ade9ed1beb82c3
# Parent  f5aa712e6250d5bae6e70e6fb6d41adcf1b8bad7
tuned;

diff -r f5aa712e6250 -r 8fcc23e8e1d9 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Jan 09 20:26:59 2017 +0100
+++ b/src/Pure/Tools/build.scala	Mon Jan 09 20:31:00 2017 +0100
@@ -97,11 +97,11 @@
 
   object Session_Content
   {
-    def empty: Session_Content =
+    val empty: Session_Content =
       Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty,
         Nil, Graph_Display.empty_graph)
 
-    def bootstrap: Session_Content =
+    lazy val bootstrap: Session_Content =
       Session_Content(Set.empty, Map.empty, Thy_Header.bootstrap_header,
         Thy_Header.bootstrap_syntax, Nil, Graph_Display.empty_graph)
   }