diff -r d9527f97246e -r 89669c58e506 Univ.ML
--- a/Univ.ML	Thu Aug 25 10:47:33 1994 +0200
+++ b/Univ.ML	Thu Aug 25 11:01:45 1994 +0200
@@ -496,9 +496,11 @@
 
 (*** Equality : the diagonal relation ***)
 
-goalw Univ.thy [diag_def] "!!a A. a:A ==> <a,a> : diag(A)";
-by (REPEAT (ares_tac [singletonI,UN_I] 1));
-val diagI = result();
+goalw Univ.thy [diag_def] "!!a A. [| a=b;  a:A |] ==> <a,b> : diag(A)";
+by (fast_tac set_cs 1);
+val diag_eqI = result();
+
+val diagI = refl RS diag_eqI |> standard;
 
 (*The general elimination rule*)
 val major::prems = goalw Univ.thy [diag_def]