--- a/src/FOL/ex/If.ML Tue Jan 07 16:29:43 1997 +0100
+++ b/src/FOL/ex/If.ML Wed Jan 08 12:14:53 1997 +0100
@@ -11,13 +11,13 @@
val prems = goalw If.thy [if_def]
"[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
-by (fast_tac (FOL_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
qed "ifI";
val major::prems = goalw If.thy [if_def]
"[| if(P,Q,R); [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
by (cut_facts_tac [major] 1);
-by (fast_tac (FOL_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
qed "ifE";