src/Pure/context.ML
changeset 29367 741373421318
parent 29095 a75f3ed534a0
child 29368 503ce3f8f092
     1.1 --- a/src/Pure/context.ML	Tue Jan 06 13:46:48 2009 +0100
     1.2 +++ b/src/Pure/context.ML	Tue Jan 06 14:33:49 2009 +0100
     1.3 @@ -132,7 +132,15 @@
     1.4  
     1.5  val copy_data = Datatab.map' invoke_copy;
     1.6  val extend_data = Datatab.map' invoke_extend;
     1.7 -fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
     1.8 +
     1.9 +fun merge_data pp (data1, data2) =
    1.10 +  Datatab.keys (Datatab.merge (K true) (data1, data2))
    1.11 +  |> ParList.map (fn k =>
    1.12 +    (case (Datatab.lookup data1 k, Datatab.lookup data2 k) of
    1.13 +      (SOME x, NONE) => (k, invoke_extend k x)
    1.14 +    | (NONE, SOME y) => (k, invoke_extend k y)
    1.15 +    | (SOME x, SOME y) => (k, invoke_merge pp k (invoke_extend k x, invoke_extend k y))))
    1.16 +  |> Datatab.make;
    1.17  
    1.18  end;
    1.19