# HG changeset patch
# User haftmann
# Date 1236465664 -3600
# Node ID f977e10af7e2326d643d74070061bea90b2fb0bc
# Parent  d9ecd70b111298ad81b54a18074c865a8d5465c1# Parent  047f183c43b0005f98f7d57648b7f65eb24fe7e3
merged

diff -r 047f183c43b0 -r f977e10af7e2 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Mar 07 15:20:32 2009 +0100
+++ b/src/HOL/HOL.thy	Sat Mar 07 23:41:04 2009 +0100
@@ -1710,8 +1710,6 @@
 
 text {* This will be relocated once Nitpick is moved to HOL. *}
 
-consts nitpick_maybe :: "'a \<Rightarrow> 'a" ("_\<^isub>?" [40] 40)
-
 ML {*
 structure Nitpick_Const_Def_Thms = NamedThmsFun
 (
diff -r 047f183c43b0 -r f977e10af7e2 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sat Mar 07 15:20:32 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Sat Mar 07 23:41:04 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}
@@ -1227,7 +1231,7 @@
           SatSolver.SATISFIABLE assignment =>
           (Output.priority ("*** Model found: ***\n" ^ print_model thy model
             (fn i => case assignment i of SOME b => b | NONE => true));
-           "genuine")
+           if maybe_spurious then "potential" else "genuine")
         | SatSolver.UNSATISFIABLE _ =>
           (Output.priority "No model exists.";
           case next_universe universe sizes minsize maxsize of