# HG changeset patch
# User blanchet
# Date 1309288019 -7200
# Node ID 0940a64beca277576a91f1d09c3eba89de0a2491
# Parent  8e3e933b3c69fff3c5ec85f78f14aad4cf4278fa
reenabled accidentally-disabled automatic minimization

diff -r 8e3e933b3c69 -r 0940a64beca2 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Jun 28 20:42:29 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Jun 28 21:06:59 2011 +0200
@@ -70,7 +70,7 @@
   Attrib.setup_config_int @{binding sledgehammer_auto_min_min_facts}
       (fn generic => Config.get_generic generic binary_min_facts)
 val auto_min_max_time =
-  Attrib.setup_config_real @{binding sledgehammer_auto_min_max_time} (K 0.0) (*###*)
+  Attrib.setup_config_real @{binding sledgehammer_auto_min_max_time} (K 5.0)
 
 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)