values_timeout defaults to 600.0 on SML/NJ -- saves us from cluttering all theories equivalent declarations
authorkrauss
Tue, 19 Jul 2011 00:07:21 +0200
changeset 43896 8955dcac6c71
parent 43895 09576fe8ef08
child 43897 b28745c3ddce
values_timeout defaults to 600.0 on SML/NJ -- saves us from cluttering all theories equivalent declarations
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)