src/Pure/context.ML

     val k = serial ();
     val kind = {empty = empty, extend = extend, merge = merge};
     val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
   in k end;
 
-val extend_data = Datatab.map' invoke_extend;
+val extend_data = Datatab.map invoke_extend;
 
 fun merge_data pp (data1, data2) =
   Datatab.keys (Datatab.merge (K true) (data1, data2))
   |> Par_List.map (fn k =>
     (case (Datatab.lookup data1 k, Datatab.lookup data2 k) of

   (case Datatab.lookup (! kinds) k of
     SOME init => init
   | NONE => raise Fail "Invalid proof data identifier");
 
 fun init_data thy =
-  Datatab.map' (fn k => fn _ => invoke_init k thy) (! kinds);
+  Datatab.map (fn k => fn _ => invoke_init k thy) (! kinds);
 
 fun init_new_data data thy =
   Datatab.merge (K true) (data, init_data thy);
 
 in