clean Nitpick's wellfoundedness cache once in a while, to avoid potential memory leak

--- a/doc-src/Nitpick/nitpick.tex	Tue Oct 27 16:52:06 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Tue Oct 27 17:53:19 2009 +0100
@@ -2398,11 +2398,11 @@
 & \textit{subgoal}\end{aligned}$
 \postw
 
+\let\antiq=\textrm
+
 \subsection{Registration of Coinductive Datatypes}
 \label{registration-of-coinductive-datatypes}
 
-\let\antiq=\textrm
-
 If you have defined a custom coinductive datatype, you can tell Nitpick about
 it, so that it can use an efficient Kodkod axiomatization similar to the one it
 uses for lazy lists. The interface for registering and unregistering coinductive

--- 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 =>