src/Pure/Syntax/syntax.ML
changeset 41711 3422ae5aff3a
parent 41377 390c53904220
child 42043 2055515c9d3f
--- a/src/Pure/Syntax/syntax.ML	Sat Feb 05 18:09:57 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Feb 05 20:38:32 2011 +0100
@@ -756,7 +756,7 @@
             \Retry with smaller syntax_ambiguity_level for more information."
           else "";
 
-        val errs = Par_List.map check ts;
+        val errs = Par_List.map_name "Syntax.disambig" check ts;
         val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
         val len = length results;