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