# HG changeset patch
# User lcp
# Date 797162769 -7200
# Node ID be30ddf0c9b47dc81c867e9c2c3df47d34b517a0
# Parent  db0563a1644a2c9cd73d05b3ca3478d2882ec1ab
Deleted call to flexflex_tac

diff -r db0563a1644a -r be30ddf0c9b4 src/ZF/EquivClass.ML
--- a/src/ZF/EquivClass.ML	Thu Apr 06 12:03:01 1995 +0200
+++ b/src/ZF/EquivClass.ML	Thu Apr 06 12:06:09 1995 +0200
@@ -39,7 +39,6 @@
 by (fast_tac (ZF_cs addSIs [converseI] addIs [compI]) 3);
 by (ALLGOALS (fast_tac 
 	      (ZF_cs addSIs [converseI] addIs [compI] addSEs [compE])));
-by flexflex_tac;
 qed "comp_equivI";
 
 (** Equivalence classes **)