# HG changeset patch
# User blanchet
# Date 1266940393 -3600
# Node ID b83b9f2a4b923ae680d381e2226c782b6309b591
# Parent  f61de25f71f9e677002fbec1c4ae9fde803c261b
show Kodkod warning message even in non-verbose mode

diff -r f61de25f71f9 -r b83b9f2a4b92 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 23 15:56:13 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 23 16:53:13 2010 +0100
@@ -583,7 +583,7 @@
                 o nth problems)
     (* string -> unit *)
     fun show_kodkod_warning "" = ()
-      | show_kodkod_warning s = print_v (fn () => "Kodkod warning: " ^ s ^ ".")
+      | show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".")
 
     (* bool -> KK.raw_bound list -> problem_extension -> bool option *)
     fun print_and_check_model genuine bounds