1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -628,6 +628,8 @@
     1.4     Linux appears to be the only ATP that does not honor its time limit. *)
     1.5  val atp_timeout_slack = seconds 1.0
     1.6  
     1.7 +val mono_max_privileged_facts = 10
     1.8 +
     1.9  fun run_atp mode name
    1.10          ({exec, required_vars, arguments, proof_delims, known_failures,
    1.11            prem_role, best_slices, best_max_mono_iters,
    1.12 @@ -701,7 +703,7 @@
    1.13                    Logic.list_implies (hyp_ts, concl_t)
    1.14                    |> Skip_Proof.make_thm thy
    1.15                  val rths =
    1.16 -                  facts |> chop (length facts div 4)
    1.17 +                  facts |> chop mono_max_privileged_facts
    1.18                          |>> map (pair 1 o snd)
    1.19                          ||> map (pair 2 o snd)
    1.20                          |> op @