# HG changeset patch
# User wenzelm
# Date 1415375496 -3600
# Node ID 4aa9b3ab0b403971cd07d02964a4c7075f615bb0
# Parent  23d0ffd4800671cec8a852b5383667f133a55b6c
tuned;

diff -r 23d0ffd48006 -r 4aa9b3ab0b40 src/HOL/Tools/Nitpick/nitpick_util.ML
--- 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