# HG changeset patch
# User wenzelm
# Date 1190124488 -7200
# Node ID c7da302a03467d29be00096781113794f14d1b6d
# Parent  351a308ab58df6d13f96ba68e28a564b3d9d5de0
reactivated tests in smlnj;

diff -r 351a308ab58d -r c7da302a0346 src/HOL/Complex/ex/ROOT.ML
--- a/src/HOL/Complex/ex/ROOT.ML	Tue Sep 18 16:08:00 2007 +0200
+++ b/src/HOL/Complex/ex/ROOT.ML	Tue Sep 18 16:08:08 2007 +0200
@@ -20,9 +20,9 @@
   "Arithmetic_Series_Complex",
   "HarmonicSeries",
 
-  "DenumRat"
+  "DenumRat",
+  
+  "MIR",
+  "ReflectedFerrack"
 ];
 
-if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
-else use_thys ["MIR", "ReflectedFerrack"];
-