# HG changeset patch
# User wenzelm
# Date 1309445426 -7200
# Node ID 16482dc641d471bc84e6714a25f757f79f41522a
# Parent  20760e3608fa3426d70fd02791cd77b93c024f83
back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);

diff -r 20760e3608fa -r 16482dc641d4 src/Pure/context.ML
--- a/src/Pure/context.ML	Thu Jun 30 16:07:30 2011 +0200
+++ b/src/Pure/context.ML	Thu Jun 30 16:50:26 2011 +0200
@@ -153,15 +153,7 @@
   in k end;
 
 val extend_data = Datatab.map invoke_extend;
-
-fun merge_data pp (data1, data2) =
-  Datatab.keys (Datatab.merge (K true) (data1, data2))
-  |> Par_List.map_name "Context.merge_data" (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;
+fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
 
 end;