diff -r 44660100931d -r 84f283385091 src/Pure/Tools/build_history.scala
--- a/src/Pure/Tools/build_history.scala	Tue Oct 04 18:09:23 2016 +0200
+++ b/src/Pure/Tools/build_history.scala	Tue Oct 04 18:26:26 2016 +0200
@@ -119,7 +119,10 @@
       val platform_64 = isabelle("getenv -b ISABELLE_PLATFORM64").check.out
       val platform_family = isabelle("getenv -b ISABELLE_PLATFORM_FAMILY").check.out
 
-      val polyml_home = Path.explode(isabelle("getenv -b ML_HOME").check.out).dir
+      val polyml_home =
+        try { Path.explode(isabelle("getenv -b ML_HOME").check.out).dir }
+        catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) }
+
       def ml_home(platform: String): Path = polyml_home + Path.explode(platform)
 
       def err(platform: String): Nothing =