src/Pure/context.ML
changeset 43610 16482dc641d4
parent 42818 128cc195ced3
child 43684 85388f5570c4
     1.1 --- a/src/Pure/context.ML	Thu Jun 30 16:07:30 2011 +0200
     1.2 +++ b/src/Pure/context.ML	Thu Jun 30 16:50:26 2011 +0200
     1.3 @@ -153,15 +153,7 @@
     1.4    in k end;
     1.5  
     1.6  val extend_data = Datatab.map invoke_extend;
     1.7 -
     1.8 -fun merge_data pp (data1, data2) =
     1.9 -  Datatab.keys (Datatab.merge (K true) (data1, data2))
    1.10 -  |> Par_List.map_name "Context.merge_data" (fn k =>
    1.11 -    (case (Datatab.lookup data1 k, Datatab.lookup data2 k) of
    1.12 -      (SOME x, NONE) => (k, invoke_extend k x)
    1.13 -    | (NONE, SOME y) => (k, invoke_extend k y)
    1.14 -    | (SOME x, SOME y) => (k, invoke_merge pp k (invoke_extend k x, invoke_extend k y))))
    1.15 -  |> Datatab.make;
    1.16 +fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
    1.17  
    1.18  end;
    1.19