# HG changeset patch
# User wenzelm
# Date 1222346252 -7200
# Node ID 5d79c5d684596f1d85686fcdfdf5dd8ff6c6396d
# Parent  80d4d40eecf97f119a07394cd1ccc150896819ef
tuned comments;

diff -r 80d4d40eecf9 -r 5d79c5d68459 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Thu Sep 25 14:35:03 2008 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Thu Sep 25 14:37:32 2008 +0200
@@ -11,7 +11,7 @@
     time.  The overhead of scheduling is significantly higher than
     just traversing the list of operands sequentially.
 
-  * The order of operator application is non-determined.  Watch out
+  * The order of operator application is non-deterministic.  Watch out
     for operators that have side-effects or raise exceptions!
 *)