diff -r 2fb2d48de366 -r d57bfb44c9e5 src/Pure/Concurrent/par_list_dummy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/par_list_dummy.ML	Thu Oct 09 20:53:13 2008 +0200
@@ -0,0 +1,17 @@
+(*  Title:      Pure/Concurrent/par_list_dummy.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Dummy version of parallel list combinators -- plain sequential evaluation.
+*)
+
+structure ParList: PAR_LIST =
+struct
+
+val map = map;
+val get_some = get_first;
+val fins_some = find_first;
+val exists = exists;
+val forall = forall;
+
+end;