# HG changeset patch
# User berghofe
# Date 835357148 -7200
# Node ID c192d7dc22e78b0d965b8d5b1fa5c21cfdd8f4e4
# Parent  bc506bcb9fe45508951971261dcd33f412cd31ca
Replaced occurrence of set_cs by claset_of "Fun" .

diff -r bc506bcb9fe4 -r c192d7dc22e7 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");