# HG changeset patch
# User haftmann
# Date 1159964747 -7200
# Node ID 7f6f26d8349b71afb8387028f09cbd9ec72d880a
# Parent  9f7f0bf89e7d11f881c31527f94352370d4f4767
insert replacing ins ins_int ins_string

diff -r 9f7f0bf89e7d -r 7f6f26d8349b NEWS
--- a/NEWS	Wed Oct 04 14:17:47 2006 +0200
+++ b/NEWS	Wed Oct 04 14:25:47 2006 +0200
@@ -627,6 +627,11 @@
 
 *** ML ***
 
+* Pure/library:
+
+infixes ins ins_string ins_int have been abandoned in favour of insert.
+INCOMPATIBILITY: rewrite "x ins(_...) xs" to "insert (op =) x xs"
+
 * Pure/General/susp.ML:
 
 New module for delayed evaluations.