src/ZF/Trancl.ML

--- a/src/ZF/Trancl.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Trancl.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -55,7 +55,7 @@
 qed "r_subset_rtrancl";
 
 goal Trancl.thy "field(r^*) = field(r)";
-by (fast_tac (eq_cs addIs [r_into_rtrancl] 
+by (fast_tac (!claset addIs [r_into_rtrancl] 
                     addSDs [rtrancl_type RS subsetD]) 1);
 qed "rtrancl_field";