disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
authorwenzelm
Sun, 10 Jun 2007 21:06:59 +0200
changeset 23301 4c7e6d295980
parent 23300 b785068bd5dc
child 23302 919d5c1fe509
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
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";