merged

--- a/src/HOL/Tools/record.ML	Wed Oct 21 15:54:31 2009 +0200
+++ b/src/HOL/Tools/record.ML	Wed Oct 21 16:57:57 2009 +0200
@@ -2323,8 +2323,7 @@
     val final_thy =
       thms_thy
       |> (snd oo PureThy.add_thmss)
-          [((Binding.name "simps", sel_upd_simps),
-            [Simplifier.simp_add, Nitpick_Const_Simps.add]),
+          [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
            ((Binding.name "iffs", iffs), [iff_add])]
       |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
       |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')

--- a/src/HOL/Tools/refute.ML	Wed Oct 21 15:54:31 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Wed Oct 21 16:57:57 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;