1.1 --- a/src/HOL/Fun.ML	Fri Jun 21 13:34:55 1996 +0200
     1.2 +++ b/src/HOL/Fun.ML	Fri Jun 21 13:39:08 1996 +0200
     1.3 @@ -189,4 +189,4 @@
     1.4      addEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
     1.5              subsetD, subsetCE];
     1.6  
     1.7 -fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;
     1.8 +fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac (claset_of "Fun");