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

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 11:24:16 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 11:24:54 2011 +0200
     2.3 @@ -546,12 +546,6 @@
     2.4    #> Config.put Monomorph.max_new_instances max_new_instances
     2.5    #> Config.put Monomorph.keep_partial_instances false
     2.6  
     2.7 -fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
     2.8 -  (not debug ? Config.put SMT_Config.verbose false)
     2.9 -  #> Config.put SMT_Config.monomorph_limit max_mono_iters
    2.10 -  #> Config.put SMT_Config.monomorph_instances max_mono_instances
    2.11 -  #> Config.put SMT_Config.monomorph_full false
    2.12 -
    2.13  fun run_atp mode name
    2.14          ({exec, required_execs, arguments, proof_delims, known_failures,
    2.15            conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
    2.16 @@ -891,8 +885,8 @@
    2.17          val timer = Timer.startRealTimer ()
    2.18          val state =
    2.19            state |> Proof.map_context
    2.20 -                       (repair_smt_monomorph_context debug max_mono_iters
    2.21 -                            (max_new_mono_instances + length facts))
    2.22 +                       (repair_monomorph_context max_mono_iters
    2.23 +                                                 max_new_mono_instances)
    2.24          val ms = timeout |> Time.toMilliseconds
    2.25          val slice_timeout =
    2.26            if slice < max_slices then