# HG changeset patch
# User wenzelm
# Date 1489746478 -3600
# Node ID 6934d0878634666e671fb2c935090ce7f77bc077
# Parent  75999f2a0c3849416a2bded8579624f3f762096c
tuned;

diff -r 75999f2a0c38 -r 6934d0878634 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Mar 17 11:15:57 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 17 11:27:58 2017 +0100
@@ -599,11 +599,8 @@
     def find_log_gz(name: String): Option[Path] =
       input_dirs.map(_ + log_gz(name)).find(_.is_file)
 
-    def find_heap(name: String): Option[Path] =
-      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
-
     def heap(name: String): Path =
-      find_heap(name) getOrElse
+      input_dirs.map(_ + Path.basic(name)).find(_.is_file) getOrElse
         error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
           cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))