src/Pure/context.ML
changeset 29368 503ce3f8f092
parent 29367 741373421318
child 30628 4078276bcace
     1.1 --- a/src/Pure/context.ML	Tue Jan 06 14:33:49 2009 +0100
     1.2 +++ b/src/Pure/context.ML	Tue Jan 06 14:43:35 2009 +0100
     1.3 @@ -135,7 +135,7 @@
     1.4  
     1.5  fun merge_data pp (data1, data2) =
     1.6    Datatab.keys (Datatab.merge (K true) (data1, data2))
     1.7 -  |> ParList.map (fn k =>
     1.8 +  |> Par_List.map (fn k =>
     1.9      (case (Datatab.lookup data1 k, Datatab.lookup data2 k) of
    1.10        (SOME x, NONE) => (k, invoke_extend k x)
    1.11      | (NONE, SOME y) => (k, invoke_extend k y)