values_timeout defaults to 600.0 on SML/NJ -- saves us from cluttering all theories equivalent declarations
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Jul 18 23:48:28 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Jul 19 00:07:21 2011 +0200
@@ -1570,7 +1570,10 @@
(* values_timeout configuration *)
-val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K 20.0)
+val default_values_timeout =
+ if String.isPrefix "smlnj" (getenv "ML_SYSTEM") then 600.0 else 20.0
+
+val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
val setup = PredData.put (Graph.empty) #>
Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)