merged

--- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Jun 07 11:24:16 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Jun 07 11:24:54 2011 +0200
@@ -243,7 +243,7 @@
               o generic_metis_tac type_syss ctxt (schem_facts @ ths))
   end
 
-fun setup_method (binding, type_syss as type_sys :: _) =
+fun setup_method (binding, type_syss) =
   (if type_syss = metis_default_type_syss then
      (Args.parens Parse.short_ident
       >> (fn s => AList.lookup (op =) type_sys_aliases s |> the_default s))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 11:24:16 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 11:24:54 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