# HG changeset patch
# User wenzelm
# Date 1267273925 -3600
# Node ID 11f58c600707fdeed0a66238674d8d7d58df06e2
# Parent  2f83aa48d6967b7ab3af715ae9b1dfcac5da9047
parallel brute-force disambiguation;

diff -r 2f83aa48d696 -r 11f58c600707 src/Pure/Syntax/syntax.ML
--- 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