author | wenzelm |
Sat, 27 Feb 2010 13:32:05 +0100 | |
changeset 35394 | 11f58c600707 |
parent 35393 | 2f83aa48d696 |
child 35395 | ba804f4c82c6 |
--- a/src/Pure/Syntax/syntax.ML Sat Feb 27 13:31:55 2010 +0100 +++ b/src/Pure/Syntax/syntax.ML Sat Feb 27 13:32:05 2010 +0100 @@ -533,7 +533,7 @@ \Retry with smaller Syntax.ambiguity_level for more information." else ""; - val errs = map check ts; + val errs = Par_List.map check ts; val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs); val len = length results; in