# HG changeset patch
# User paulson
# Date 852722093 -3600
# Node ID 750499529c05bd86c90b05490c01e22d47ed6379
# Parent  c4368c967c565955bed7162248a32fd82d3bc9ac
Removed some (not all!) uses of FOL_cs

diff -r c4368c967c56 -r 750499529c05 src/FOL/ex/If.ML
--- 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";