# HG changeset patch
# User blanchet
# Date 1307438032 -7200
# Node ID a1a0dcbeb785a2fefdcf3326184d6c20c018d94c
# Parent  3a8d49bc06e12249fbee9526c76d1417a8a20567
move away from old SMT monomorphizer

diff -r 3a8d49bc06e1 -r a1a0dcbeb785 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 11:12:52 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 11:13:52 2011 +0200
@@ -546,12 +546,6 @@
   #> Config.put Monomorph.max_new_instances max_new_instances
   #> Config.put Monomorph.keep_partial_instances false
 
-fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
-  (not debug ? Config.put SMT_Config.verbose false)
-  #> Config.put SMT_Config.monomorph_limit max_mono_iters
-  #> Config.put SMT_Config.monomorph_instances max_mono_instances
-  #> Config.put SMT_Config.monomorph_full false
-
 fun run_atp mode name
         ({exec, required_execs, arguments, proof_delims, known_failures,
           conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
@@ -891,8 +885,8 @@
         val timer = Timer.startRealTimer ()
         val state =
           state |> Proof.map_context
-                       (repair_smt_monomorph_context debug max_mono_iters
-                            (max_new_mono_instances + length facts))
+                       (repair_monomorph_context max_mono_iters
+                                                 max_new_mono_instances)
         val ms = timeout |> Time.toMilliseconds
         val slice_timeout =
           if slice < max_slices then