# HG changeset patch
# User wenzelm
# Date 1372886769 -7200
# Node ID 89c5af70553f447bcdbebad8e64f440c4f4ea196
# Parent  b5b3c888df9f98952d726c3a2cd56cf8f7795d13
tuned message;

diff -r b5b3c888df9f -r 89c5af70553f src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Wed Jul 03 23:02:00 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Jul 03 23:26:09 2013 +0200
@@ -318,7 +318,8 @@
           (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
             "\nproduces " ^ string_of_int len ^ " parse trees" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-            map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))];
+            map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
+              (take limit pts))];
 
   in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end;
 
@@ -389,7 +390,7 @@
           val checked = map snd (proper_results results');
           val checked_len = length checked;
 
-          val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
+          val pretty_term = Syntax.pretty_term (Config.put Printer.show_brackets true ctxt);
         in
           if checked_len = 0 then
             report_result ctxt pos []
@@ -408,7 +409,8 @@
                 (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^
                   (if checked_len <= limit then ""
                    else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-                  map show_term (take limit checked))))))]
+                  map (Pretty.string_of o Pretty.item o single o pretty_term)
+                    (take limit checked))))))]
         end handle ERROR msg => parse_failed ctxt pos msg kind)
   end;