# HG changeset patch
# User paulson
# Date 835968655 -7200
# Node ID 791e794739668596a0a683decffe22a58c84bb83
# Parent  a6d7aef48c2f7c58878939edc8967ee5229377ae
Removed a use of eq_cs

diff -r a6d7aef48c2f -r 791e79473966 src/HOL/IOA/meta_theory/IOA.ML
--- a/src/HOL/IOA/meta_theory/IOA.ML	Fri Jun 28 15:29:39 1996 +0200
+++ b/src/HOL/IOA/meta_theory/IOA.ML	Fri Jun 28 15:30:55 1996 +0200
@@ -105,7 +105,7 @@
 "actions(asig_comp a b) = actions(a) Un actions(b)";
   by(simp_tac (!simpset addsimps
                ([actions_def,asig_comp_def]@asig_projections)) 1);
-  by(fast_tac eq_cs 1);
+  by(Fast_tac 1);
 qed "actions_asig_comp";
 
 goal IOA.thy
diff -r a6d7aef48c2f -r 791e79473966 src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Fri Jun 28 15:29:39 1996 +0200
+++ b/src/HOL/Integ/Equiv.ML	Fri Jun 28 15:30:55 1996 +0200
@@ -129,7 +129,7 @@
 (** Not needed by Theory Integ --> bypassed **)
 (**goalw Equiv.thy [equiv_def,refl_def,quotient_def]
     "!!A r. equiv A r ==> Union(A/r) = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Union_quotient";
 **)
 
@@ -147,7 +147,7 @@
 
 (* theorem needed to prove UN_equiv_class *)
 goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 qed "UN_singleton_lemma";
 val UN_singleton = ballI RSN (2,UN_singleton_lemma);