parallel brute-force disambiguation;
authorwenzelm
Sat, 27 Feb 2010 13:32:05 +0100
changeset 3539411f58c600707
parent 35393 2f83aa48d696
child 35395 ba804f4c82c6
parallel brute-force disambiguation;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Feb 27 13:31:55 2010 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Feb 27 13:32:05 2010 +0100
     1.3 @@ -533,7 +533,7 @@
     1.4              \Retry with smaller Syntax.ambiguity_level for more information."
     1.5            else "";
     1.6  
     1.7 -        val errs = map check ts;
     1.8 +        val errs = Par_List.map check ts;
     1.9          val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
    1.10          val len = length results;
    1.11        in