src/Pure/context.ML
changeset 29368 503ce3f8f092
parent 29367 741373421318
child 30628 4078276bcace
--- a/src/Pure/context.ML	Tue Jan 06 14:33:49 2009 +0100
+++ b/src/Pure/context.ML	Tue Jan 06 14:43:35 2009 +0100
@@ -135,7 +135,7 @@
 
 fun merge_data pp (data1, data2) =
   Datatab.keys (Datatab.merge (K true) (data1, data2))
-  |> ParList.map (fn k =>
+  |> Par_List.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)