--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 24 12:31:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 24 14:43:35 2010 +0100
@@ -346,7 +346,7 @@
fun monotonicity_message Ts extra =
let val ss = map (quote o string_for_type ctxt) Ts in
"The type" ^ plural_s_for_list ss ^ " " ^
- space_implode " " (serial_commas "and" ss) ^ " " ^
+ space_implode " " (Sledgehammer_Util.serial_commas "and" ss) ^ " " ^
(if none_true monos then
"passed the monotonicity test"
else
@@ -684,7 +684,8 @@
options
in
print ("Try again with " ^
- space_implode " " (serial_commas "and" ss) ^
+ space_implode " "
+ (Sledgehammer_Util.serial_commas "and" ss) ^
" to confirm that the " ^ das_wort_model ^
" is genuine.")
end