# HG changeset patch
# User wenzelm
# Date 1459529034 -7200
# Node ID ddc58826cbe958db618dfb7949d60ea59f631f3f
# Parent  f9d102ef13f19ef567200919e66a944eeb42fbe2
tuned messages;

diff -r f9d102ef13f1 -r ddc58826cbe9 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 18:32:52 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 18:43:54 2016 +0200
@@ -178,9 +178,6 @@
 
 in
 
-fun show_props props =
-  commas_quote (map #1 props) ^ Position.here_list (map (#2 o #2) props);
-
 fun read_properties ss =
   let
     val props =
@@ -188,9 +185,10 @@
         (props, []) => props
       | (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos));
     val _ =
-      (case duplicates (eq_fst op =) props of
+      (case AList.group (op =) props |> filter (fn (_, [_]) => false | _ => true) of
         [] => ()
-      | dups => error ("Duplicate properties: " ^ show_props dups));
+      | dups => error ("Duplicate properties: " ^ commas_quote (map #1 dups) ^
+          Position.here_list (map #2 (maps #2 dups))));
   in props end;
 
 val get_string = get_property "" I;
@@ -221,7 +219,8 @@
     val markup = (markup_name, map (apsnd #1) markup_props);
     val _ =
       if markup_name = "" andalso not (null markup_props) then
-        error ("Markup name required for block properties: " ^ show_props markup_props)
+        error ("Markup name required for block properties: " ^
+          commas_quote (map #1 markup_props) ^ Position.here_list (map (#2 o #2) markup_props))
       else ();
 
     val consistent = get_bool Markup.consistentN props;