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 447678955dcac6c71
parent 44766 09576fe8ef08
child 44768 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
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jul 18 23:48:28 2011 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Jul 19 00:07:21 2011 +0200
     1.3 @@ -1570,7 +1570,10 @@
     1.4  
     1.5  (* values_timeout configuration *)
     1.6  
     1.7 -val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K 20.0)
     1.8 +val default_values_timeout =
     1.9 +  if String.isPrefix "smlnj" (getenv "ML_SYSTEM") then 600.0 else 20.0
    1.10 +
    1.11 +val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
    1.12  
    1.13  val setup = PredData.put (Graph.empty) #>
    1.14    Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)