# HG changeset patch
# User wenzelm
# Date 1507458960 -7200
# Node ID dac4cfbfede8b3571104b8ee953c78fd8441297b
# Parent  bf54ca580bf2bf464222eec3fa9ea2d66c466b36
proper output of raw ML;

diff -r bf54ca580bf2 -r dac4cfbfede8 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) +