Removed some (not all!) uses of FOL_cs
authorpaulson
Wed, 08 Jan 1997 12:14:53 +0100
changeset 2486 750499529c05
parent 2485 c4368c967c56
child 2487 4f0bf2936bc0
Removed some (not all!) uses of FOL_cs
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";