diff -r b7dd670cfe3a -r a1a18530c4ac src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Jan 17 18:19:57 1997 +0100
+++ b/src/Pure/library.ML	Fri Jan 17 18:20:22 1997 +0100
@@ -611,6 +611,12 @@
         | over [] = [p]
   in over al end;
 
+fun gen_overwrite eq (al, p as (key, _)) =
+  let fun over ((q as (keyi, _)) :: pairs) =
+            if eq (keyi, key) then p :: pairs else q :: (over pairs)
+        | over [] = [p]
+  in over al end;
+
 
 
 (** generic tables **)