--- a/src/HOL/Mirabelle/ROOT.ML Wed Sep 02 22:12:40 2009 +0200
+++ b/src/HOL/Mirabelle/ROOT.ML Thu Sep 03 14:05:13 2009 +0200
@@ -1,1 +1,2 @@
-use_thy "MirabelleTest";
+if can (unprefix "polyml") (getenv "ML_SYSTEM") then use_thy "MirabelleTest"
+else ();