# HG changeset patch
# User wenzelm
# Date 1399559324 -7200
# Node ID f371418b96411868b8520d5e63856bbdebb8da63
# Parent  df4cd6e1fdfae11bb63b9b60247ad0131cb71b5f
tuned message;

diff -r df4cd6e1fdfa -r f371418b9641 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu May 08 16:19:16 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Thu May 08 16:28:44 2014 +0200
@@ -70,7 +70,7 @@
     | Solves => Pretty.str (prfx "solves")
     | Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
         Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))]
-    | Pattern pat => Pretty.enclose (prfx " \"") "\""
+    | Pattern pat => Pretty.enclose (prfx "\"") "\""
         [Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)])
   end;