src/HOL/Finite.ML

--- a/src/HOL/Finite.ML	Mon Jun 03 11:44:44 1996 +0200
+++ b/src/HOL/Finite.ML	Mon Jun 03 17:10:56 1996 +0200
@@ -49,7 +49,7 @@
             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";
@@ -205,47 +205,47 @@
 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 |] ==> \
@@ -316,7 +316,7 @@
 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);