# HG changeset patch
# User krauss
# Date 1311026841 -7200
# Node ID 8955dcac6c71e57fd182623b55ea239758269e39
# Parent  09576fe8ef0847be502031ff35eadc80a88119aa
values_timeout defaults to 600.0 on SML/NJ -- saves us from cluttering all theories equivalent declarations

diff -r 09576fe8ef08 -r 8955dcac6c71 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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)