insert replacing ins ins_int ins_string

--- 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.