# HG changeset patch
# User lcp
# Date 799062119 -7200
# Node ID 68f088887f48e7d5b96bfa706aca210aef494ed5
# Parent  848bf2e18dff499557757bba9acf8d887b433e94
Modified proofs for new claset primitives.  The problem is that they enforce
the "most recent added rule has priority" policy more strictly now.

diff -r 848bf2e18dff -r 68f088887f48 src/ZF/EquivClass.ML
--- a/src/ZF/EquivClass.ML	Fri Apr 28 11:31:33 1995 +0200
+++ b/src/ZF/EquivClass.ML	Fri Apr 28 11:41:59 1995 +0200
@@ -79,7 +79,7 @@
 qed "equiv_class_nondisjoint";
 
 goalw EquivClass.thy [equiv_def] "!!A r. equiv(A,r) ==> r <= A*A";
-by (safe_tac ZF_cs);
+by (safe_tac subset_cs);
 qed "equiv_type";
 
 goal EquivClass.thy