src/Pure/ML/ml_console.scala

--- a/src/Pure/ML/ml_console.scala	Wed Nov 01 16:38:15 2017 +0100
+++ b/src/Pure/ML/ml_console.scala	Wed Nov 01 16:43:51 2017 +0100
@@ -75,7 +75,7 @@
           raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
           session_base =
             if (raw_ml_system) None
-            else Some(Sessions.session_base_info(options, logic, dirs).check_base))
+            else Some(Sessions.base_info(options, logic, dirs).check_base))
       val process_output = Future.thread[Unit]("process_output") {
         try {
           var result = new StringBuilder(100)