Replaced occurrence of set_cs by claset_of "Fun" .
authorberghofe
Fri Jun 21 13:39:08 1996 +0200 (1996-06-21)
changeset 1822c192d7dc22e7
parent 1821 bc506bcb9fe4
child 1823 e1458e1a9f80
Replaced occurrence of set_cs by claset_of "Fun" .
src/HOL/Fun.ML
     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");