--- a/src/Pure/context.ML Tue Jan 06 13:46:48 2009 +0100
+++ b/src/Pure/context.ML Tue Jan 06 14:33:49 2009 +0100
@@ -132,7 +132,15 @@
val copy_data = Datatab.map' invoke_copy;
val extend_data = Datatab.map' invoke_extend;
-fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
+
+fun merge_data pp (data1, data2) =
+ Datatab.keys (Datatab.merge (K true) (data1, data2))
+ |> ParList.map (fn k =>
+ (case (Datatab.lookup data1 k, Datatab.lookup data2 k) of
+ (SOME x, NONE) => (k, invoke_extend k x)
+ | (NONE, SOME y) => (k, invoke_extend k y)
+ | (SOME x, SOME y) => (k, invoke_merge pp k (invoke_extend k x, invoke_extend k y))))
+ |> Datatab.make;
end;