back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);

--- 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;