# HG changeset patch
# User boehmes
# Date 1307475460 -7200
# Node ID f4d15a58ed8b8d08334b2360be42c0f33bc212e2
# Parent  c729110a9f087c62c504fb29b6524d63dd86ea21
clarified (and slightly modified) the semantics of max_new_instances

diff -r c729110a9f08 -r f4d15a58ed8b src/HOL/Tools/monomorph.ML
--- a/src/HOL/Tools/monomorph.ML	Tue Jun 07 19:22:52 2011 +0200
+++ b/src/HOL/Tools/monomorph.ML	Tue Jun 07 21:37:40 2011 +0200
@@ -206,7 +206,12 @@
 
 fun make_subst_ctxt ctxt thm_infos known_grounds substitutions =
   let
-    val limit = Config.get ctxt max_new_instances
+    (* The total limit of returned (ground) facts is the number of facts
+       given to the monomorphizer increased by max_new_instances.  Since
+       initially ground facts are returned anyway, the limit here is not
+       counting them. *)
+    val limit = Config.get ctxt max_new_instances + 
+      fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos 0
 
     fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
       | add_ground_consts (Schematic _) = I