make the monomorphizer more predictable by making the cutoff independent on the number of facts

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