# HG changeset patch
# User wenzelm
# Date 1605474256 -3600
# Node ID 5fc193537b7c6d78e531e909951e2eb625471946
# Parent  217e6cf61453a1aaa71ad051fbfbaad82c8e7853
tuned;

diff -r 217e6cf61453 -r 5fc193537b7c src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sun Nov 15 22:00:45 2020 +0100
+++ b/src/Pure/ML/ml_process.scala	Sun Nov 15 22:04:16 2020 +0100
@@ -85,10 +85,10 @@
       session_base match {
         case None => ""
         case Some(base) =>
-          def print_table(table: List[(String, String)]): String =
+          def print_table: List[(String, String)] => String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
-                ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
+                ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))
           def print_list: List[String] => String =
             ML_Syntax.print_list(ML_Syntax.print_string_bytes)
           def print_sessions: List[(String, Position.T)] => String =