# HG changeset patch
# User blanchet
# Date 1378743161 -7200
# Node ID 0721fc9d0fe79b1963a7a07652506906eb63fa07
# Parent  247817dbb9906036904e51f9048c5dda5afcf3b1
made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents

diff -r 247817dbb990 -r 0721fc9d0fe7 src/HOL/Tools/monomorph.ML
--- a/src/HOL/Tools/monomorph.ML	Mon Sep 09 15:22:04 2013 +0200
+++ b/src/HOL/Tools/monomorph.ML	Mon Sep 09 18:12:41 2013 +0200
@@ -77,9 +77,6 @@
     fun round i x = if i > max then x else round (i + 1) (f ctxt i x)
   in round 1 end
 
-fun reached_new_instance_limit ctxt n =
-  n >= Config.get ctxt max_new_instances
-
 fun reached_thm_instance_limit ctxt n =
   n >= Config.get ctxt max_thm_instances
 
@@ -183,28 +180,31 @@
   in Term.fold_aterms add (Thm.prop_of thm) end
 
 
-fun add_insts ctxt round used_grounds new_grounds id thm tvars schematics cx =
+fun add_insts max_instances ctxt round used_grounds new_grounds id thm tvars
+    schematics cx =
   let
     exception ENOUGH of
       typ list Symtab.table * (int * (int * thm) list Inttab.table)
 
     val thy = Proof_Context.theory_of ctxt
 
-    fun add subst (next_grounds, (n, insts)) =
-      let
-        val thm' = instantiate thy subst thm
-        val rthm = (round, thm')
-        val rthms = Inttab.lookup_list insts id;
-        val n_insts' =
-          if member (eq_snd Thm.eq_thm) rthms rthm orelse
-             reached_thm_instance_limit ctxt (length rthms) then
-            (n, insts)
-          else
-            (n + 1, Inttab.cons_list (id, rthm) insts)
-        val next_grounds' =
-          add_new_grounds used_grounds new_grounds thm' next_grounds
-        val cx' = (next_grounds', n_insts')
-      in if reached_new_instance_limit ctxt n then raise ENOUGH cx' else cx' end
+    fun add subst (cx as (next_grounds, (n, insts))) =
+      if n >= max_instances then
+        raise ENOUGH cx
+      else
+        let
+          val thm' = instantiate thy subst thm
+          val rthm = (round, thm')
+          val rthms = Inttab.lookup_list insts id;
+          val n_insts' =
+            if member (eq_snd Thm.eq_thm) rthms rthm orelse
+               reached_thm_instance_limit ctxt (length rthms) then
+              (n, insts)
+            else
+              (n + 1, Inttab.cons_list (id, rthm) insts)
+          val next_grounds' =
+            add_new_grounds used_grounds new_grounds thm' next_grounds
+        in (next_grounds', n_insts') end
 
     fun with_grounds (n, T) f subst (n', Us) =
       let
@@ -250,12 +250,12 @@
 fun is_active round initial_round = (round > initial_round)
 
 
-fun find_instances thm_infos ctxt round (known_grounds, new_grounds, insts) =
+fun find_instances max_instances thm_infos ctxt round
+    (known_grounds, new_grounds, insts) =
   let
-    val add_new = add_insts ctxt round
+    val add_new = add_insts max_instances ctxt round
     fun consider_all pred f (cx as (_, (n, _))) =
-      if reached_new_instance_limit ctxt n then cx
-      else fold_schematics pred f thm_infos cx
+      if n >= max_instances then cx else fold_schematics pred f thm_infos cx
 
     val known_grounds' = Symtab.merge_list (op =) (known_grounds, new_grounds)
     val empty_grounds = clear_grounds known_grounds'
@@ -277,9 +277,12 @@
   let
     val known_grounds = fold_grounds add_ground_types thm_infos consts
     val empty_grounds = clear_grounds known_grounds
+    val max_instances =
+      Config.get ctxt max_new_instances
+      |> fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos
   in
     (empty_grounds, known_grounds, (0, Inttab.empty))
-    |> limit_rounds ctxt (find_instances thm_infos)
+    |> limit_rounds ctxt (find_instances max_instances thm_infos)
     |> (fn (_, _, (_, insts)) => insts)
   end