src/HOL/Tools/Nitpick/nitpick_hol.ML

   can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
        #> SINGLE (DETERM_TIMEOUT timeout
                                  (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 []
 
 val termination_tacs = [Lexicographic_Order.lex_order_tac,

                    priority ("Wellfoundedness goal: " ^
                              Syntax.string_of_term ctxt prop ^ ".")
                  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 =>
            let
              val goal = prop |> cterm_of thy |> Goal.init