# HG changeset patch
# User blanchet
# Date 1289223210 -3600
# Node ID fb6ee11e776a284538ef3c55eea0e69f0085fd29
# Parent  3d93bd33304dba83196d5e7674c5f446ea2c96d3
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving

diff -r 3d93bd33304d -r fb6ee11e776a src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 08 13:53:18 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 08 14:33:30 2010 +0100
@@ -418,6 +418,7 @@
 val smt_iter_fact_divisor = 2
 val smt_iter_min_msecs = 5000
 val smt_iter_timeout_divisor = 2
+val smt_monomorph_limit = 4
 
 fun smt_filter_loop iter outcome0 msecs_so_far remote timeout state facts i =
   let
@@ -458,10 +459,14 @@
        used_facts = used_facts, run_time_in_msecs = msecs_so_far}
   end
 
-fun run_smt_solver auto remote ({timeout, ...} : params) minimize_command
+fun run_smt_solver auto remote ({debug, timeout, ...} : params) minimize_command
                    ({state, subgoal, subgoal_count, facts, ...}
                     : prover_problem) =
   let
+    val repair_context =
+      Config.put SMT_Config.verbose debug
+      #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
+    val state = state |> Proof.map_context repair_context
     val ctxt = Proof.context_of state
     val {outcome, used_facts, run_time_in_msecs} =
       smt_filter_loop 1 NONE (SOME 0) remote timeout state