Replaced occurrence of set_cs by claset_of "Fun" .
authorberghofe
Fri, 21 Jun 1996 13:39:08 +0200
changeset 1822 c192d7dc22e7
parent 1821 bc506bcb9fe4
child 1823 e1458e1a9f80
Replaced occurrence of set_cs by claset_of "Fun" .
src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Jun 21 13:34:55 1996 +0200
+++ b/src/HOL/Fun.ML	Fri Jun 21 13:39:08 1996 +0200
@@ -189,4 +189,4 @@
     addEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
             subsetD, subsetCE];
 
-fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;
+fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac (claset_of "Fun");