--- a/src/HOL/equalities.ML Wed Nov 25 14:11:24 1998 +0100
+++ b/src/HOL/equalities.ML Wed Nov 25 15:51:53 1998 +0100
@@ -108,6 +108,7 @@
Goal "(%x. x) `` Y = Y";
by (Blast_tac 1);
qed "image_id";
+Addsimps [image_id];
Goal "f``(g``A) = (%x. f (g x)) `` A";
by (Blast_tac 1);