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