--- a/src/HOL/ex/rel.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/rel.ML Fri Jun 21 12:18:50 1996 +0200
@@ -34,7 +34,7 @@
(*** domain ***)
val [prem] = goalw Rel.thy [domain_def,Pair_def] "(a,b): r ==> a : domain(r)";
-by (fast_tac (set_cs addIs [prem]) 1);
+by (fast_tac (!claset addIs [prem]) 1);
qed "domainI";
val major::prems = goalw Rel.thy [domain_def]
@@ -48,7 +48,7 @@
(*** range2 ***)
val [prem] = goalw Rel.thy [range2_def,Pair_def] "(a,b): r ==> b : range2(r)";
-by (fast_tac (set_cs addIs [prem]) 1);
+by (fast_tac (!claset addIs [prem]) 1);
qed "range2I";
val major::prems = goalw Rel.thy [range2_def]
@@ -102,8 +102,8 @@
\ ==> wf(r)";
by (rtac (prem1 RS wfI) 1);
by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);
-by (fast_tac ZF_cs 3);
-by (fast_tac ZF_cs 2);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 3);
+by (Fast_tac 2);
+by (Fast_tac 1);
qed "wfI2";