Now Un_insert_left, Un_insert_right are default rewrite rules

--- a/src/HOL/equalities.ML	Mon Jun 02 12:13:42 1997 +0200
+++ b/src/HOL/equalities.ML	Mon Jun 02 12:14:15 1997 +0200
@@ -228,10 +228,12 @@
 goal Set.thy "(insert a B) Un C = insert a (B Un C)";
 by (Blast_tac 1);
 qed "Un_insert_left";
+Addsimps[Un_insert_left];
 
 goal Set.thy "A Un (insert a B) = insert a (A Un B)";
 by (Blast_tac 1);
 qed "Un_insert_right";
+Addsimps[Un_insert_right];
 
 goal Set.thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
 \                                          else        B Int C)";