# HG changeset patch
# User wenzelm
# Date 1231248829 -3600
# Node ID 741373421318920d2f26acc4653aaae36cb10f39
# Parent  1ffc8cbf39ecc33ea44a7b56d302975427939ef7
parallelized merge_data;

diff -r 1ffc8cbf39ec -r 741373421318 src/Pure/context.ML
--- 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;