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;