values_timeout defaults to 600.0 on SML/NJ -- saves us from cluttering all theories equivalent declarations
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)