--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 27 16:52:06 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 27 17:53:19 2009 +0100
@@ -1606,6 +1606,7 @@
(tac ctxt (auto_tac (clasimpset_of ctxt))))
#> the #> Goal.finish ctxt) goal
+val max_cached_wfs = 100
val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
val cached_wf_props : (term * bool) list Unsynchronized.ref =
Unsynchronized.ref []
@@ -1639,8 +1640,11 @@
else
()
in
- if tac_timeout = (!cached_timeout) then ()
- else (cached_wf_props := []; cached_timeout := tac_timeout);
+ if tac_timeout = (!cached_timeout)
+ andalso length (!cached_wf_props) < max_cached_wfs then
+ ()
+ else
+ (cached_wf_props := []; cached_timeout := tac_timeout);
case AList.lookup (op =) (!cached_wf_props) prop of
SOME wf => wf
| NONE =>