diff -r 946ef711dc7d -r fce515f7759c src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Feb 16 18:25:55 2006 +0100
+++ b/src/Pure/General/table.ML	Thu Feb 16 18:25:56 2006 +0100
@@ -48,7 +48,6 @@
   val delete_safe: key -> 'a table -> 'a table
   val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool
   val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table    (*exception DUP*)
-  val replace: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table
   val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
   val lookup_list: 'a list table -> key -> 'a list
   val update_list: (key * 'a) -> 'a list table -> 'a list table
@@ -341,9 +340,6 @@
 fun insert eq (key, x) =
   modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else raise DUP key);
 
-fun replace eq (key, x) =
-  modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else x);
-
 fun remove eq (key, x) tab =
   (case lookup tab key of
     NONE => tab