src/HOL/Finite.ML

 by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)",
             rtac mp, etac spec,
             rtac subs]);
 by (rtac (fin RS Fin_induct) 1);
 by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
-by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
+by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1]));
 by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
 by (ALLGOALS Asm_simp_tac);
 qed "Fin_subset";
 
 goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";

 by (rtac exI 1);
 by (rtac (refl RS disjI2 RS conjI) 1);
 by (etac equalityE 1);
 by (asm_full_simp_tac
      (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
-by (SELECT_GOAL(safe_tac eq_cs)1);
+by (SELECT_GOAL(safe_tac (!claset))1);
   by (Asm_full_simp_tac 1);
   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
-  by (SELECT_GOAL(safe_tac eq_cs)1);
+  by (SELECT_GOAL(safe_tac (!claset))1);
    by (subgoal_tac "x ~= f m" 1);
     by (Fast_tac 2);
    by (subgoal_tac "? k. f k = x & k<m" 1);
-    by (best_tac set_cs 2);
-   by (SELECT_GOAL(safe_tac HOL_cs)1);
+    by (best_tac (!claset) 2);
+   by (SELECT_GOAL(safe_tac (!claset))1);
    by (res_inst_tac [("x","k")] exI 1);
    by (Asm_simp_tac 1);
   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-  by (best_tac set_cs 1);
+  by (best_tac (!claset) 1);
  bd sym 1;
  by (rotate_tac ~1 1);
  by (Asm_full_simp_tac 1);
  by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
- by (SELECT_GOAL(safe_tac eq_cs)1);
+ by (SELECT_GOAL(safe_tac (!claset))1);
   by (subgoal_tac "x ~= f m" 1);
    by (Fast_tac 2);
   by (subgoal_tac "? k. f k = x & k<m" 1);
-   by (best_tac set_cs 2);
-  by (SELECT_GOAL(safe_tac HOL_cs)1);
+   by (best_tac (!claset) 2);
+  by (SELECT_GOAL(safe_tac (!claset))1);
   by (res_inst_tac [("x","k")] exI 1);
   by (Asm_simp_tac 1);
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
- by (best_tac set_cs 1);
+ by (best_tac (!claset) 1);
 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
-by (SELECT_GOAL(safe_tac eq_cs)1);
+by (SELECT_GOAL(safe_tac (!claset))1);
  by (subgoal_tac "x ~= f i" 1);
   by (Fast_tac 2);
  by (case_tac "x = f m" 1);
   by (res_inst_tac [("x","i")] exI 1);
   by (Asm_simp_tac 1);
  by (subgoal_tac "? k. f k = x & k<m" 1);
-  by (best_tac set_cs 2);
- by (SELECT_GOAL(safe_tac HOL_cs)1);
+  by (best_tac (!claset) 2);
+ by (SELECT_GOAL(safe_tac (!claset))1);
  by (res_inst_tac [("x","k")] exI 1);
  by (Asm_simp_tac 1);
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (best_tac set_cs 1);
+by (best_tac (!claset) 1);
 val lemma = result();
 
 goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
 \ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
 by (rtac Least_equality 1);

 by (etac finite_induct 1);
 by (Simp_tac 1);
 by (strip_tac 1);
 by (case_tac "x:B" 1);
  by (dtac mk_disjoint_insert 1);
- by (SELECT_GOAL(safe_tac HOL_cs)1);
+ by (SELECT_GOAL(safe_tac (!claset))1);
  by (rotate_tac ~1 1);
  by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
 by (rotate_tac ~1 1);
 by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
 qed_spec_mp "card_mono";