best_tac, deepen_tac and safe_tac now also use default claset.

--- a/src/HOL/Arith.ML	Mon Jun 03 11:44:44 1996 +0200
+++ b/src/HOL/Arith.ML	Mon Jun 03 17:10:56 1996 +0200
@@ -384,7 +384,7 @@
 goal thy "Suc(Suc(m)) mod 2 = m mod 2";
 by (subgoal_tac "m mod 2 < 2" 1);
 by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
-by (safe_tac less_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_Suc])));
 qed "mod2_Suc_Suc";
 Addsimps [mod2_Suc_Suc];
@@ -406,7 +406,7 @@
 by (REPEAT_FIRST (ares_tac [conjI, impI]));
 by (res_inst_tac [("x","0")] exI 2);
 by (Simp_tac 2);
-by (safe_tac HOL_cs);
+by (safe_tac (claset_of "HOL"));
 by (res_inst_tac [("x","Suc(k)")] exI 1);
 by (Simp_tac 1);
 qed_spec_mp "less_eq_Suc_add";
@@ -462,7 +462,7 @@
 qed_spec_mp "add_leD1";
 
 goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
-by (safe_tac (HOL_cs addSDs [less_eq_Suc_add]));
+by (safe_tac (!claset addSDs [less_eq_Suc_add]));
 by (asm_full_simp_tac
     (!simpset delsimps [add_Suc_right]
                 addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
@@ -523,7 +523,7 @@
 goal Arith.thy "!!i::nat. [| i<=j; k<=l |] ==> i*k<=j*l";
 by (rtac le_trans 1);
 by (ALLGOALS 
-    (deepen_tac (HOL_cs addIs [mult_commute RS ssubst, mult_le_mono1]) 0));
+    (deepen_tac (!claset addIs [mult_commute RS ssubst, mult_le_mono1]) 0));
 qed "mult_le_mono";
 
 (*strict, in 1st argument; proof is by induction on k>0*)

--- 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);

--- a/src/HOL/Nat.ML	Mon Jun 03 11:44:44 1996 +0200
+++ b/src/HOL/Nat.ML	Mon Jun 03 17:10:56 1996 +0200
@@ -557,7 +557,7 @@
 	cut_facts_tac prems 1,
 	rtac select_equality 1,
 	fold_goals_tac [Least_def],
-	safe_tac (HOL_cs addSEs [LeastI]),
+	safe_tac (!claset addSEs [LeastI]),
 	res_inst_tac [("n","j")] natE 1,
 	Fast_tac 1,
 	fast_tac (!claset addDs [Suc_less_SucD] addDs [not_less_Least]) 1,	
@@ -566,11 +566,11 @@
 	hyp_subst_tac 1,
 	rewtac Least_def,
 	rtac (select_equality RS arg_cong RS sym) 1,
-	safe_tac HOL_cs,
+	safe_tac (!claset),
 	dtac Suc_mono 1,
 	Fast_tac 1,
 	cut_facts_tac [less_linear] 1,
-	safe_tac HOL_cs,
+	safe_tac (!claset),
 	atac 2,
 	Fast_tac 2,
 	dtac Suc_mono 1,

--- a/src/HOL/Relation.ML	Mon Jun 03 11:44:44 1996 +0200
+++ b/src/HOL/Relation.ML	Mon Jun 03 17:10:56 1996 +0200
@@ -162,7 +162,7 @@
     "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS CollectE) 1),
-    (safe_tac set_cs),
+    (safe_tac (!claset)),
     (etac RangeE 1),
     (rtac (hd prems) 1),
     (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);

--- a/src/HOL/Trancl.ML	Mon Jun 03 11:44:44 1996 +0200
+++ b/src/HOL/Trancl.ML	Mon Jun 03 17:10:56 1996 +0200
@@ -75,7 +75,7 @@
 
 (*transitivity of transitive closure!! -- by induction.*)
 goalw Trancl.thy [trans_def] "trans(r^*)";
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (eres_inst_tac [("b","z")] rtrancl_induct 1);
 by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
 qed "trans_rtrancl";
@@ -150,7 +150,7 @@
 qed "rtrancl_converseI";
 
 goal Trancl.thy "(converse r)^* = converse(r^*)";
-by (safe_tac (rel_eq_cs addSIs [rtrancl_converseI]));
+by (safe_tac (!claset addSIs [rtrancl_converseI]));
 by (res_inst_tac [("p","x")] PairE 1);
 by (hyp_subst_tac 1);
 by (etac rtrancl_converseD 1);

--- a/src/HOL/Univ.ML	Mon Jun 03 11:44:44 1996 +0200
+++ b/src/HOL/Univ.ML	Mon Jun 03 17:10:56 1996 +0200
@@ -131,7 +131,7 @@
 by (etac (Push_inject1 RS sym) 1);
 by (rtac (inj_Rep_Node RS injD) 1);
 by (etac trans 1);
-by (safe_tac (HOL_cs addSEs [Pair_inject,Push_inject,sym]));
+by (safe_tac (!claset addSEs [Pair_inject,Push_inject,sym]));
 qed "Push_Node_inject";
 
 
@@ -230,7 +230,7 @@
     "ndepth (Push_Node i n) = Suc(ndepth(n))";
 by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1);
 by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (etac ssubst 1);  (*instantiates type variables!*)
 by (Simp_tac 1);
 by (rtac Least_equality 1);
@@ -244,11 +244,11 @@
 (*** ntrunc applied to the various node sets ***)
 
 goalw Univ.thy [ntrunc_def] "ntrunc 0 M = {}";
-by (safe_tac (set_cs addSIs [equalityI] addSEs [less_zeroE]));
+by (safe_tac (!claset addSIs [equalityI] addSEs [less_zeroE]));
 qed "ntrunc_0";
 
 goalw Univ.thy [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)";
-by (safe_tac (set_cs addSIs [equalityI]));
+by (safe_tac (!claset addSIs [equalityI]));
 by (stac ndepth_K0 1);
 by (rtac zero_less_Suc 1);
 qed "ntrunc_Atom";
@@ -263,7 +263,7 @@
 
 goalw Univ.thy [Scons_def,ntrunc_def]
     "ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N";
-by (safe_tac (set_cs addSIs [equalityI,imageI]));
+by (safe_tac ((claset_of "Fun") addSIs [equalityI,imageI]));
 by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
 by (REPEAT (rtac Suc_less_SucD 1 THEN 
             rtac (ndepth_Push_Node RS subst) 1 THEN 
@@ -275,7 +275,7 @@
 goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
 by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
 by (rewtac Scons_def);
-by (safe_tac (set_cs addSIs [equalityI]));
+by (safe_tac (!claset addSIs [equalityI]));
 qed "ntrunc_one_In0";
 
 goalw Univ.thy [In0_def]
@@ -286,7 +286,7 @@
 goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
 by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
 by (rewtac Scons_def);
-by (safe_tac (set_cs addSIs [equalityI]));
+by (safe_tac (!claset addSIs [equalityI]));
 qed "ntrunc_one_In1";
 
 goalw Univ.thy [In1_def]
@@ -541,7 +541,7 @@
 (*Dependent version*)
 goal Univ.thy
     "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
-by (safe_tac univ_cs);
+by (safe_tac (!claset));
 by (stac Split 1);
 by (Fast_tac 1);
 qed "dprod_subset_Sigma2";

--- a/src/HOL/WF.ML	Mon Jun 03 11:44:44 1996 +0200
+++ b/src/HOL/WF.ML	Mon Jun 03 17:10:56 1996 +0200
@@ -19,7 +19,7 @@
 by (strip_tac 1);
 by (rtac allE 1);
 by (assume_tac 1);
-by (best_tac (HOL_cs addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
+by (best_tac (!claset addSEs [prem1 RS subsetD RS SigmaE2] addIs [prem2]) 1);
 qed "wfI";
 
 val major::prems = goalw WF.thy [wf_def]

--- a/src/HOL/equalities.ML	Mon Jun 03 11:44:44 1996 +0200
+++ b/src/HOL/equalities.ML	Mon Jun 03 17:10:56 1996 +0200
@@ -310,7 +310,7 @@
 qed "Inter_Un_subset";
 
 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
-by (best_tac eq_cs 1);
+by (best_tac (!claset) 1);
 qed "Inter_Un_distrib";
 
 section "UN and INT";
@@ -412,7 +412,7 @@
 qed "Un_Inter";
 
 goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
-by (best_tac eq_cs 1);
+by (best_tac (!claset) 1);
 qed "Int_Inter_image";
 
 (*Equivalent version*)