# HG changeset patch
# User wenzelm
# Date 1181502419 -7200
# Node ID 4c7e6d2959802031579bb473fef4b15a3206931b
# Parent  b785068bd5dc5b54f28562e7507a494f8a402caa
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);

diff -r b785068bd5dc -r 4c7e6d295980 src/HOL/Complex/ex/ROOT.ML
--- a/src/HOL/Complex/ex/ROOT.ML	Sun Jun 10 10:23:42 2007 +0200
+++ b/src/HOL/Complex/ex/ROOT.ML	Sun Jun 10 21:06:59 2007 +0200
@@ -22,5 +22,9 @@
 use_thy "DenumRat";
 
 use_thy "Ferrante_Rackoff_Ex";
-use_thy "MIR";
-use_thy "ReflectedFerrack";
\ No newline at end of file
+
+if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
+else use_thy "MIR";
+
+if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
+else use_thy "ReflectedFerrack";