# HG changeset patch
# User blanchet
# Date 1290693530 -3600
# Node ID 8a3f7ea9137082ad16434a8349cd35274cc7192a
# Parent  c3979dd80a50c192aff0dbf1d33de01594ff0c76
cosmetics

diff -r c3979dd80a50 -r 8a3f7ea91370 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Nov 25 14:58:20 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Nov 25 14:58:50 2010 +0100
@@ -104,8 +104,9 @@
     else is_atp_installed thy name
   end
 
-val smt_default_max_relevant = 200 (* FUDGE *)
-val auto_max_relevant_divisor = 2 (* FUDGE *)
+(* FUDGE *)
+val smt_default_max_relevant = 200
+val auto_max_relevant_divisor = 2
 
 fun default_max_relevant_for_prover thy name =
   if is_smt_prover name then smt_default_max_relevant
@@ -432,6 +433,7 @@
   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure _ = UnknownError
 
+(* FUDGE *)
 val smt_max_iter = 8
 val smt_iter_fact_divisor = 2
 val smt_iter_min_msecs = 5000