# HG changeset patch
# User blanchet
# Date 1307515663 -7200
# Node ID dd38b8ef52b9f9d1863d7488bb44b6fa52d478d7
# Parent  3baf384e2b996d2a2b40882f5fe5f8c3ca7ff4dc
exploit new semantics of "max_new_instances"

diff -r 3baf384e2b99 -r dd38b8ef52b9 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 08 08:47:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -534,15 +534,9 @@
    | _ => name)
   |> minimize_command
 
-fun is_polymorphic_fact get_thm =
-  get_thm #> prop_of #> Term.exists_type Monomorph.typ_has_tvars
-fun num_polymorphic_facts get_thm facts =
-  fold (fn fact => is_polymorphic_fact get_thm fact ? Integer.add 1) facts 0
-
-fun repair_monomorph_context max_iters get_thm facts max_new_instances =
+fun repair_monomorph_context max_iters max_new_instances =
   Config.put Monomorph.max_rounds max_iters
-  #> Config.put Monomorph.max_new_instances
-                (num_polymorphic_facts get_thm facts + max_new_instances)
+  #> Config.put Monomorph.max_new_instances max_new_instances
   #> Config.put Monomorph.keep_partial_instances false
 
 fun run_atp mode name
@@ -597,7 +591,7 @@
             fun monomorphize_facts facts =
               let
                 val ctxt =
-                  ctxt |> repair_monomorph_context max_mono_iters snd facts
+                  ctxt |> repair_monomorph_context max_mono_iters
                                                    max_new_mono_instances
                 (* pseudo-theorem involving the same constants as the subgoal *)
                 val subgoal_th =
@@ -886,8 +880,8 @@
         val timer = Timer.startRealTimer ()
         val state =
           state |> Proof.map_context
-                       (repair_monomorph_context max_mono_iters (snd o snd)
-                                                 facts max_new_mono_instances)
+                       (repair_monomorph_context max_mono_iters
+                                                 max_new_mono_instances)
         val ms = timeout |> Time.toMilliseconds
         val slice_timeout =
           if slice < max_slices then