parallel brute-force disambiguation;
authorwenzelm
Sat, 27 Feb 2010 13:32:05 +0100
changeset 35394 11f58c600707
parent 35393 2f83aa48d696
child 35395 ba804f4c82c6
parallel brute-force disambiguation;
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