# HG changeset patch
# User blanchet
# Date 1299077482 -3600
# Node ID 10fd9e5d58ba1c04f555d6d3e4d69751a0bd52e5
# Parent  394eef237bd109c3568bc7ae07384fb4a9edfb84
added missing spaces in output

diff -r 394eef237bd1 -r 10fd9e5d58ba src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 02 14:50:16 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 02 15:51:22 2011 +0100
@@ -714,7 +714,7 @@
                         options
                 in
                   print ("Try again with " ^
-                         implode (serial_commas "and" ss) ^
+                         space_implode " " (serial_commas "and" ss) ^
                          " to confirm that the " ^ das_wort_model ^
                          " is genuine.")
                 end