diff -r 41a117825097 -r dfbd51a5eab1 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Apr 10 23:58:07 2015 +0200
+++ b/src/HOL/ROOT	Sat Apr 11 12:24:51 2015 +0200
@@ -806,7 +806,7 @@
   theories Mirabelle_Test
 
 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
-  options [document = false, timeout = 60]
+  options [condition = ML_SYSTEM_POLYML, document = false, timeout = 60]
   theories Ex
 
 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +