tuned;

--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 07 16:36:55 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 07 16:51:36 2014 +0100
@@ -289,7 +289,7 @@
 
 fun pretty_maybe_quote keywords pretty =
   let val s = Pretty.str_of pretty in
-    if maybe_quote keywords s = s then pretty else Pretty.enum "" "\"" "\"" [pretty]
+    if maybe_quote keywords s = s then pretty else Pretty.quote pretty
   end
 
 val hashw = ATP_Util.hashw