src/Pure/ML/ml_process.scala

--- a/src/Pure/ML/ml_process.scala	Sat Oct 07 20:31:01 2017 +0200
+++ b/src/Pure/ML/ml_process.scala	Sun Oct 08 12:36:00 2017 +0200
@@ -98,9 +98,9 @@
           def print_table(table: List[(String, String)]): String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
-                ML_Syntax.print_string, ML_Syntax.print_string))(table)
+                ML_Syntax.print_string0, ML_Syntax.print_string0))(table)
           def print_list(list: List[String]): String =
-            ML_Syntax.print_list(ML_Syntax.print_string)(list)
+            ML_Syntax.print_list(ML_Syntax.print_string0)(list)
           List("Resources.init_session_base" +
             " {global_theories = " + print_table(base.global_theories.toList) +
             ", loaded_theories = " + print_list(base.loaded_theories.keys) +