# HG changeset patch
# User wenzelm
# Date 1415960354 -3600
# Node ID 6573e6d64ec89441ecf532affa8ef30790060c1e
# Parent  44afb337bb9291d15b41368700fe4a268667b173
proper sequential version (cf. 302104d8366b);

diff -r 44afb337bb92 -r 6573e6d64ec8 src/Pure/Concurrent/par_list_sequential.ML
--- a/src/Pure/Concurrent/par_list_sequential.ML	Fri Nov 14 08:18:58 2014 +0100
+++ b/src/Pure/Concurrent/par_list_sequential.ML	Fri Nov 14 11:19:14 2014 +0100
@@ -10,6 +10,7 @@
 fun managed_results _ f = map (Exn.capture f);
 fun map_name _ = map;
 val map = map;
+val map_independent = map;
 val get_some = get_first;
 val find_some = find_first;
 val exists = exists;