src/Pure/ML/ml_process.scala
changeset 71875 aaa984499d36
parent 71639 ec84f542e411
child 71876 ad063ac1f617
--- a/src/Pure/ML/ml_process.scala	Sun May 24 10:28:04 2020 +0200
+++ b/src/Pure/ML/ml_process.scala	Sun May 24 10:36:42 2020 +0200
@@ -92,7 +92,7 @@
             ML_Syntax.print_list(
               ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
 
-          List("Resources.init_session_base" +
+          List("Resources.init_session" +
             " {session_positions = " + print_sessions(sessions_structure.session_positions) +
             ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
             ", docs = " + print_list(base.doc_names) +