Added a second timeout mechanism to Refute.
For some reason, TimeLimit.timeLimit often does not work, and it
leaves Refute running forever, making any evaluation using
Mutabelle or Mirabelle impossible. The redundant timeout seems to
do the trick.

--- a/src/HOL/Tools/refute.ML	Sat Mar 07 12:27:26 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Sat Mar 07 16:47:36 2009 +0100
@@ -1165,6 +1165,7 @@
     (* unit -> unit *)
     fun wrapper () =
     let
+      val timer  = Timer.startRealTimer ()
       val u      = unfold_defs thy t
       val _      = Output.tracing ("Unfolded term: " ^
                                    Syntax.string_of_term_global thy u)
@@ -1201,6 +1202,9 @@
       (* (Term.typ * int) list -> string *)
       fun find_model_loop universe =
       let
+        val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer)
+        val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime
+                orelse raise TimeLimit.TimeOut
         val init_model = (universe, [])
         val init_args  = {maxvars = maxvars, def_eq = false, next_idx = 1,
           bounds = [], wellformed = True}