# HG changeset patch
# User wenzelm
# Date 1372016456 -7200
# Node ID 7fa1245f50df1a43e0cc1531bc619a8a9bd2716c
# Parent  289e36c2870a9dcbd9509a001ceea94914d009c1
tuned message;

diff -r 289e36c2870a -r 7fa1245f50df src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Jun 23 21:23:36 2013 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Jun 23 21:40:56 2013 +0200
@@ -218,8 +218,8 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val morph' = morph $> export;
-    fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
-    fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
+    fun print_qual (qual, mandatory) = qual ^ (if mandatory then "!" else "?");
+    fun prt_quals qs = Pretty.str (space_implode "." (map print_qual qs));
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     fun prt_term' t =
       if Config.get ctxt show_types