# HG changeset patch
# User blanchet
# Date 1256136844 -7200
# Node ID dd1192a969684fc8184b0aec06a5492bf25b0814
# Parent  dabf9d1bb5523e4c4532c2f9ff280d05bda4a0ec
fixed the "expect" mechanism of Refute in the face of timeouts

diff -r dabf9d1bb552 -r dd1192a96968 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Wed Oct 21 16:53:00 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Wed Oct 21 16:54:04 2009 +0200
@@ -1145,6 +1145,10 @@
   fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver,
     expect} t negate =
   let
+    (* string -> unit *)
+    fun check_expect outcome_code =
+      if expect = "" orelse outcome_code = expect then ()
+      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
     (* unit -> unit *)
     fun wrapper () =
     let
@@ -1237,8 +1241,7 @@
           "unknown")
         val outcome_code = find_model_loop (first_universe types sizes minsize)
       in
-        if expect = "" orelse outcome_code = expect then ()
-        else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+        check_expect outcome_code
       end
     in
       (* some parameter sanity checks *)
@@ -1261,9 +1264,10 @@
         TimeLimit.timeLimit (Time.fromSeconds maxtime)
           wrapper ()
         handle TimeLimit.TimeOut =>
-          priority ("Search terminated, time limit (" ^
-            string_of_int maxtime
-            ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.")
+          (priority ("Search terminated, time limit (" ^
+              string_of_int maxtime
+              ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
+           check_expect "unknown")
       ) else
         wrapper ()
     end;