diff -r 4d00bbd3d3ac -r b2ecd577b8a3 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Mon Nov 30 10:45:39 1998 +0100
+++ b/src/HOL/Relation.ML	Tue Dec 01 10:39:02 1998 +0100
@@ -294,7 +294,7 @@
 by (Blast_tac 1);
 qed "Image_Id";
 
-Goal "B<=A ==> diag A ^^ B = B";
+Goal "diag A ^^ B = A Int B";
 by (Blast_tac 1);
 qed "Image_diag";