# HG changeset patch
# User wenzelm
# Date 1596826922 -7200
# Node ID d00220799735fd13292c0a0896d2158612934333
# Parent  2d9e40cfe9afea331951ca9189d44be262fdc713
tuned names;

diff -r 2d9e40cfe9af -r d00220799735 src/Pure/ML/ml_pid.ML
--- a/src/Pure/ML/ml_pid.ML	Fri Aug 07 20:28:53 2020 +0200
+++ b/src/Pure/ML/ml_pid.ML	Fri Aug 07 21:02:02 2020 +0200
@@ -11,7 +11,7 @@
 
 if ML_System.platform_is_windows then ML
 \<open>
-structure ML_PID: ML_PID =
+structure ML_Pid: ML_PID =
 struct
 
 val get =
@@ -22,7 +22,7 @@
 \<close>
 else ML
 \<open>
-structure ML_PID: ML_PID =
+structure ML_Pid: ML_PID =
 struct
 
 val get = Posix.ProcEnv.getpid #> Posix.Process.pidToWord #> SysWord.toLargeInt
diff -r 2d9e40cfe9af -r d00220799735 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Fri Aug 07 20:28:53 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Aug 07 21:02:02 2020 +0200
@@ -201,7 +201,7 @@
 
     fun protocol () =
      (Session.init_protocol_handlers ();
-      Output.protocol_message (Markup.ml_pid (ML_PID.get ())) [];
+      Output.protocol_message (Markup.ml_pid (ML_Pid.get ())) [];
       message Markup.initN [] [XML.Text (Session.welcome ())];
       protocol_loop ());