# HG changeset patch
# User wenzelm
# Date 1181512107 -7200
# Node ID 919d5c1fe509a02e0ba802ace2ec444c0ec5169b
# Parent  4c7e6d2959802031579bb473fef4b15a3206931b
disabled theory "Reflected_Presburger" for smlnj (temporarily);

diff -r 4c7e6d295980 -r 919d5c1fe509 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Sun Jun 10 21:06:59 2007 +0200
+++ b/src/HOL/ex/ROOT.ML	Sun Jun 10 23:48:27 2007 +0200
@@ -49,7 +49,8 @@
 time_use_thy "mesontest2";
 time_use_thy "Arith_Examples";
 time_use_thy "PresburgerEx";
-time_use_thy "Reflected_Presburger";
+if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
+else time_use_thy "Reflected_Presburger";
 time_use_thy "BT";
 time_use_thy "InSort";
 time_use_thy "Qsort";