src/HOL/Mirabelle/ROOT.ML

--- a/src/HOL/Mirabelle/ROOT.ML	Thu Sep 03 18:41:58 2009 +0200
+++ b/src/HOL/Mirabelle/ROOT.ML	Thu Sep 03 22:47:31 2009 +0200
@@ -1,3 +1,1 @@
-if String.isPrefix "polyml" ml_system
-then use_thy "MirabelleTest"
-else ();
+use_thy "MirabelleTest";