| changeset 62359 | 6709e51d5c11 |
| parent 62357 | ab76bd43c14a |
| child 62360 | 3fd79fcdb491 |
| 62357:ab76bd43c14a | 62359:6709e51d5c11 |
|---|---|
1 (* Title: Pure/Concurrent/par_list_sequential.ML |
|
2 Author: Makarius |
|
3 |
|
4 Dummy version of parallel list combinators -- plain sequential evaluation. |
|
5 *) |
|
6 |
|
7 structure Par_List: PAR_LIST = |
|
8 struct |
|
9 |
|
10 fun managed_results _ f = map (Exn.capture f); |
|
11 fun map_name _ = map; |
|
12 val map = map; |
|
13 val map_independent = map; |
|
14 val get_some = get_first; |
|
15 val find_some = find_first; |
|
16 val exists = exists; |
|
17 val forall = forall; |
|
18 |
|
19 end; |