diff -r 49d1ea25f1a4 -r faa452d8e265 src/Pure/ML-Systems/ml_system.ML
--- a/src/Pure/ML-Systems/ml_system.ML	Mon Aug 17 23:16:03 2015 +0200
+++ b/src/Pure/ML-Systems/ml_system.ML	Mon Aug 17 23:45:12 2015 +0200
@@ -11,6 +11,7 @@
   val is_smlnj: bool
   val platform: string
   val platform_is_cygwin: bool
+  val platform_is_windows: bool
   val share_common_data: unit -> unit
   val save_state: string -> unit
 end;
@@ -24,6 +25,7 @@
 
 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
 val platform_is_cygwin = String.isSuffix "cygwin" platform;
+val platform_is_windows = String.isSuffix "windows" platform;
 
 fun share_common_data () = ();
 fun save_state _ = raise Fail "Cannot save state -- undefined operation";