# HG changeset patch
# User oheimb
# Date 856025551 -3600
# Node ID e9b203f854ae11f90c593ce356652edfe4005f5c
# Parent  4b30dbe4a0209af807600c5504ceefa170c20628
reflecting my recent changes of the simplifier and classical reasoner

diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Message.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -825,13 +825,6 @@
 (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
 val pushes = pushKeys@pushCrypts;
 
-
-(*No premature instantiation of variables during simplification.
-  For proving "possibility" properties.*)
-fun safe_solver prems =
-    match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
-    ORELSE' etac FalseE;
-
 val Fake_insert_tac = 
     dresolve_tac [impOfSubs Fake_analz_insert,
                   impOfSubs Fake_parts_insert] THEN'
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/NS_Public.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -12,6 +12,8 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
+val op addss = op unsafe_addss;
+
 AddIffs [Spy_in_lost];
 
 (*Replacing the variable by a constant improves search speed by 50%!*)
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -16,6 +16,8 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
+val op addss = op unsafe_addss;
+
 AddIffs [Spy_in_lost];
 
 (*Replacing the variable by a constant improves search speed by 50%!*)
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/NS_Shared.ML
--- a/src/HOL/Auth/NS_Shared.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -113,7 +113,7 @@
       (!claset addIs [impOfSubs analz_subset_parts]
                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
-               addss (!simpset)) 1);
+               unsafe_addss (!simpset)) 1);
 (*NS2, NS4, NS5*)
 by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs addss (!simpset)) 1));
 qed_spec_mp "new_keys_not_used";
@@ -167,7 +167,7 @@
 \            | X : analz (sees lost Spy evs)";
 by (case_tac "A : lost" 1);
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
-                      addss (!simpset)) 1);
+                      unsafe_addss (!simpset)) 1);
 by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1);
 by (fast_tac (!claset addEs  partsEs
                       addSDs [A_trusts_NS2, Says_Server_message_form]
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -92,9 +92,9 @@
              (*Fake message*)
              TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
                                            impOfSubs Fake_parts_insert]
-                                    addss (!simpset)) 2)) THEN
+                            unsafe_addss (!simpset)) 2)) THEN
      (*Base case*)
-     fast_tac (!claset addss (!simpset)) 1 THEN
+     fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
      ALLGOALS Asm_simp_tac) i;
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -134,7 +134,7 @@
       (!claset addIs [impOfSubs analz_subset_parts]
                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
-               addss (!simpset)) 1);
+               unsafe_addss (!simpset)) 1);
 (*OR1-3*)
 by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
 qed_spec_mp "new_keys_not_used";
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -123,7 +123,7 @@
       (!claset addIs [impOfSubs analz_subset_parts]
                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
-               addss (!simpset)) 1);
+               unsafe_addss (!simpset)) 1);
 (*OR3*)
 by (fast_tac (!claset addss (!simpset)) 1);
 qed_spec_mp "new_keys_not_used";
@@ -297,7 +297,7 @@
                       addIs [impOfSubs analz_subset_parts]
                       addss (!simpset addsimps [parts_insert2])) 2);
 (*Oops*) 
-by (best_tac (!claset addDs [unique_session_keys] addss (!simpset)) 3);
+by (best_tac (!claset addDs [unique_session_keys] unsafe_addss (!simpset)) 3);
 (*OR4, Fake*) 
 by (REPEAT_FIRST spy_analz_tac);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/OtwayRees_Bad.ML
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -125,7 +125,7 @@
       (!claset addIs [impOfSubs analz_subset_parts]
                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
-               addss (!simpset)) 1);
+               unsafe_addss (!simpset)) 1);
 (*OR1-3*)
 by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
 qed_spec_mp "new_keys_not_used";
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Public.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -186,7 +186,7 @@
 by (fast_tac (!claset addSEs [add_leE]) 2);
 (*Nonce case*)
 by (res_inst_tac [("x","N + Suc nat")] exI 1);
-by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
+by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
 val lemma = result();
 
 goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
@@ -198,7 +198,7 @@
 (*Tactic for possibility theorems*)
 val possibility_tac =
     REPEAT 
-    (ALLGOALS (simp_tac (!simpset setsolver safe_solver))
+    (ALLGOALS (simp_tac (!simpset setSolver safe_solver))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, Nonce_supply]));
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Recur.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -157,9 +157,9 @@
              (*Fake message*)
              TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
                                            impOfSubs Fake_parts_insert]
-                                    addss (!simpset)) 2)) THEN
+                            unsafe_addss (!simpset)) 2)) THEN
      (*Base case*)
-     fast_tac (!claset addss (!simpset)) 1 THEN
+     fast_tac (!claset unsafe_addss (!simpset)) 1 THEN
      ALLGOALS Asm_simp_tac) i;
 
 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
@@ -178,7 +178,7 @@
                       addss (!simpset addsimps [parts_insert_sees])) 2);
 (*RA2*)
 by (best_tac (!claset addSEs partsEs addSDs [parts_cut]
-                      addss (!simpset)) 1);
+                      unsafe_addss (!simpset)) 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
@@ -215,13 +215,13 @@
 by (parts_induct_tac 1);
 (*RA3*)
 by (best_tac (!claset addDs  [Key_in_keysFor_parts]
-                      addss  (!simpset addsimps [parts_insert_sees])) 2);
+                      unsafe_addss  (!simpset addsimps [parts_insert_sees])) 2);
 (*Fake*)
 by (best_tac
       (!claset addIs [impOfSubs analz_subset_parts]
                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
-               addss (!simpset)) 1);
+               unsafe_addss (!simpset)) 1);
 qed_spec_mp "new_keys_not_used";
 
 
@@ -574,5 +574,5 @@
                       addSIs [disjI2]
                       addSEs [MPair_parts]
                       addDs  [parts.Body]
-                      addss  (!simpset)) 0 1);
+                      unsafe_addss  (!simpset)) 0 1);
 qed "Cert_imp_Server_msg";
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Shared.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -140,7 +140,7 @@
 by (Step_tac 1);
 by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
 by (ALLGOALS
-    (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] 
+    (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons] 
                        setloop split_tac [expand_if]))));
 qed "UN_parts_sees_Says";
 
@@ -157,7 +157,7 @@
  "!!evs. [| Says A B (Crypt (shrK C) X) : set_of_list evs;  C : lost |] \
 \        ==> X : analz (sees lost Spy evs)";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
-                      addss (!simpset)) 1);
+                      unsafe_addss (!simpset)) 1);
 qed "Says_Crypt_lost";
 
 goal thy  
@@ -165,7 +165,7 @@
 \           X ~: analz (sees lost Spy evs) |]                     \
 \        ==> C ~: lost";
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
-                      addss (!simpset)) 1);
+                      unsafe_addss (!simpset)) 1);
 qed "Says_Crypt_not_lost";
 
 (*NEEDED??*)
@@ -267,7 +267,7 @@
 by (fast_tac (!claset addSEs [add_leE]) 2);
 (*Nonce case*)
 by (res_inst_tac [("x","N + Suc nat")] exI 1);
-by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
+by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
 val lemma = result();
 
 goal thy "EX N. Nonce N ~: used evs";
@@ -352,7 +352,7 @@
 val possibility_tac =
     REPEAT (*omit used_Says so that Nonces, Keys start from different traces!*)
     (ALLGOALS (simp_tac 
-               (!simpset delsimps [used_Says] setsolver safe_solver))
+               (!simpset delsimps [used_Says] setSolver safe_solver))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, Nonce_supply, Key_supply]));
@@ -361,7 +361,7 @@
   nonces and keys initially*)
 val basic_possibility_tac =
     REPEAT 
-    (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
+    (ALLGOALS (asm_simp_tac (!simpset setSolver safe_solver))
      THEN
      REPEAT_FIRST (resolve_tac [refl, conjI]));
 
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/WooLam.ML
--- a/src/HOL/Auth/WooLam.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/WooLam.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -26,10 +26,10 @@
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS 
           woolam.WL4 RS woolam.WL5) 2);
-by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
+by (ALLGOALS (simp_tac (!simpset setSolver safe_solver)));
 by (REPEAT_FIRST (resolve_tac [refl, conjI]));
 by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
-                                    addss (!simpset setsolver safe_solver))));
+                                    addss (!simpset setSolver safe_solver))));
 result();
 
 
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -16,6 +16,8 @@
 HOL_quantifiers := false;
 Pretty.setdepth 25;
 
+val op addss = op unsafe_addss;
+
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -17,6 +17,7 @@
 proof_timing:=true;
 HOL_quantifiers := false;
 
+val op addss = op unsafe_addss;
 
 (*A "possibility property": there are traces that reach the end*)
 goal thy 
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/IMP/Transition.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -201,7 +201,7 @@
   "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
 by (rtac (major RS rtrancl_induct2) 1);
 by (Fast_tac 1);
-by (fast_tac (!claset addIs [FB_lemma3] addbefore (split_all_tac 1)) 1);
+by (fast_tac (!claset addIs [FB_lemma3] addbefore split_all_tac) 1);
 qed_spec_mp "FB_lemma2";
 
 goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -66,7 +66,7 @@
   "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])
-                                    addsolver (cut_trans_tac))));
+                                    addSolver cut_trans_tac)));
 by (safe_tac HOL_cs);
 by (ALLGOALS trans_tac);
 qed_spec_mp "lift_lift";
@@ -76,7 +76,7 @@
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift]
                                 setloop (split_tac [expand_if,expand_nat_case])
-                                addsolver (cut_trans_tac))));
+                                addSolver cut_trans_tac)));
 by (safe_tac HOL_cs);
 by (ALLGOALS trans_tac);
 qed "lift_subst";
@@ -88,7 +88,7 @@
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
                                 setloop (split_tac [expand_if])
-                                addsolver (cut_trans_tac))));
+                                addSolver cut_trans_tac)));
 by(safe_tac (HOL_cs addSEs [nat_neqE]));
 by(ALLGOALS trans_tac);
 qed "lift_subst_lt";
@@ -106,7 +106,7 @@
 by (ALLGOALS(asm_simp_tac
       (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
                 setloop (split_tac [expand_if,expand_nat_case])
-                addsolver (cut_trans_tac))));
+                addSolver cut_trans_tac)));
 by(safe_tac (HOL_cs addSEs [nat_neqE]));
 by(ALLGOALS trans_tac);
 qed_spec_mp "subst_subst";
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Lambda/ParRed.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -83,7 +83,7 @@
   by (Simp_tac 1);
  by (etac rev_mp 1);
  by (dB.induct_tac "dB1" 1);
- by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] addss !simpset)));
+ by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] unsafe_addss (!simpset))));
 qed_spec_mp "par_beta_cd";
 
 (*** Confluence (via cd) ***)
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/MiniML/W.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -492,7 +492,7 @@
 by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","Suc n")] allE 1);
-by (best_tac (HOL_cs addSDs [mk_scheme_injective] addss (!simpset addcongs [conj_cong] 
+by (best_tac (HOL_cs addSDs [mk_scheme_injective] unsafe_addss (!simpset addcongs [conj_cong] 
     setloop (split_tac [expand_option_bind]))) 1);
 
 (* case App e1 e2 *)
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Prod.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -78,7 +78,7 @@
 end;
 
 goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
-by (fast_tac (!claset addbefore split_all_tac 1) 1);
+by (fast_tac (!claset addbefore split_all_tac) 1);
 qed "split_paired_All";
 
 goalw Prod.thy [split_def] "split c (a,b) = c a b";
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/Relation.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -173,11 +173,11 @@
     (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
 
 goal Relation.thy "R O id = R";
-by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
+by (fast_tac (!claset addbefore split_all_tac) 1);
 qed "R_O_id";
 
 goal Relation.thy "id O R = R";
-by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
+by (fast_tac (!claset addbefore split_all_tac) 1);
 qed "id_O_R";
 
 Addsimps [R_O_id,id_O_R];
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/W0/I.ML
--- a/src/HOL/W0/I.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/W0/I.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -8,6 +8,8 @@
 
 open I;
 
+val op addss = op unsafe_addss;
+
 goal thy
   "! a m s s' t n.  \
 \    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/W0/Type.ML
--- a/src/HOL/W0/Type.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/W0/Type.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -259,7 +259,7 @@
 (* case [] *)
 by (Simp_tac 1);
 (* case x#xl *)
-by (fast_tac (set_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
+by (fast_tac (set_cs unsafe_addss(!simpset setloop (split_tac [expand_if]))) 1);
 qed_spec_mp "ftv_mem_sub_ftv_list";
 Addsimps [ftv_mem_sub_ftv_list];
 
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/W0/W.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -45,7 +45,7 @@
         "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
 by (expr.induct_tac "e" 1);
 (* case Var(n) *)
-by (fast_tac (HOL_cs addss (!simpset setloop (split_tac [expand_if]))) 1);
+by (fast_tac (HOL_cs unsafe_addss(!simpset setloop (split_tac [expand_if]))) 1);
 (* case Abs e *)
 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
@@ -91,7 +91,7 @@
 \                 new_tv m s & new_tv m t";
 by (expr.induct_tac "e" 1);
 (* case Var n *)
-by (fast_tac (HOL_cs addss (!simpset 
+by (fast_tac (HOL_cs unsafe_addss (!simpset 
         addsimps [id_subst_def,list_all_nth,new_tv_list,new_tv_subst] 
         setloop (split_tac [expand_if]))) 1);
 
@@ -161,7 +161,7 @@
 by (expr.induct_tac "e" 1);
 (* case Var n *)
 by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
-    addss (!simpset setloop (split_tac [expand_if]))) 1);
+    unsafe_addss (!simpset setloop (split_tac [expand_if]))) 1);
 
 (* case Abs e *)
 by (asm_full_simp_tac (!simpset addsimps
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/WF.ML
--- a/src/HOL/WF.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/WF.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -90,7 +90,7 @@
     (cut_facts_tac hyps THEN'
        DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
                         eresolve_tac [transD, mp, allE]));
-val wf_super_ss = HOL_ss addsolver indhyp_tac;
+val wf_super_ss = HOL_ss addSolver indhyp_tac;
 
 val prems = goalw WF.thy [is_recfun_def,cut_def]
     "[| wf(r);  trans(r);  is_recfun r H a f;  is_recfun r H b g |] ==> \
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/ex/Comb.ML
--- a/src/HOL/ex/Comb.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/ex/Comb.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -55,7 +55,7 @@
 
 AddIs  contract.intrs;
 AddSEs [K_contractE, S_contractE, Ap_contractE];
-Addss  (!simpset);
+Unsafe_Addss  (!simpset);
 
 goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
 by (Fast_tac 1);
@@ -106,7 +106,7 @@
 
 AddIs  parcontract.intrs;
 AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
-Addss  (!simpset);
+Unsafe_Addss  (!simpset);
 
 (*** Basic properties of parallel contraction ***)
 
diff -r 4b30dbe4a020 -r e9b203f854ae src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/HOL/indrule.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -85,10 +85,7 @@
   simplifications.  If the premises get simplified, then the proofs will 
   fail.  This arose with a premise of the form {(F n,G n)|n . True}, which
   expanded to something containing ...&True. *)
-val min_ss = empty_ss
-      setmksimps (mksimps mksimps_pairs)
-      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
-                             ORELSE' etac FalseE);
+val min_ss = HOL_basic_ss;
 
 val quant_induct = 
     prove_goalw_cterm part_rec_defs 
diff -r 4b30dbe4a020 -r e9b203f854ae src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/Arith.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -537,7 +537,7 @@
 qed "zero_lt_mult_iff";
 
 goal Arith.thy "!!k. [| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1";
-by (best_tac (!claset addEs [natE] addss (!simpset)) 1);
+by (best_tac (!claset addEs [natE] unsafe_addss (!simpset)) 1);
 qed "mult_eq_1_iff";
 
 (*Cancellation law for division*)
@@ -576,7 +576,7 @@
 by (rtac disjCI 1);
 by (dtac sym 1);
 by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
-by (fast_tac (!claset addss (!simpset)) 1);
+by (fast_tac (!claset unsafe_addss (!simpset)) 1);
 by (fast_tac (le_cs addDs [mono_lemma] 
                     addss (!simpset addsimps [mult_1_right])) 1);
 qed "mult_eq_self_implies_10";
diff -r 4b30dbe4a020 -r e9b203f854ae src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/Epsilon.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -313,7 +313,7 @@
 goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
 by (rtac (transrec2_def RS def_transrec RS trans) 1);
 by (simp_tac (!simpset addsimps [succ_not_0, THE_eq, if_P]
-                    setsolver K Fast_tac) 1);
+                    setSolver K Fast_tac) 1);
 qed "transrec2_succ";
 
 goal thy "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
diff -r 4b30dbe4a020 -r e9b203f854ae src/ZF/List.ML
--- a/src/ZF/List.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/List.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -259,7 +259,7 @@
     [list_rec_type, map_type, map_type2, app_type, length_type, 
      rev_type, flat_type, list_add_type];
 
-simpset := !simpset setsolver (type_auto_tac list_typechecks);
+simpset := !simpset setSolver (type_auto_tac list_typechecks);
 
 
 (*** theorems about map ***)
diff -r 4b30dbe4a020 -r e9b203f854ae src/ZF/Order.ML
--- a/src/ZF/Order.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/Order.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -11,6 +11,8 @@
 
 open Order;
 
+val op addss = op unsafe_addss;
+
 (** Basic properties of the definitions **)
 
 (*needed?*)
@@ -237,11 +239,10 @@
 
 (*Rewriting with bijections and converse (function inverse)*)
 val bij_inverse_ss = 
-    !simpset setsolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type, 
+    !simpset setSolver (type_auto_tac [ord_iso_is_bij, bij_is_fun, apply_type, 
                                        bij_converse_bij, comp_fun, comp_bij])
           addsimps [right_inverse_bij, left_inverse_bij];
 
-
 (** Symmetry and Transitivity Rules **)
 
 (*Reflexivity of similarity*)
diff -r 4b30dbe4a020 -r e9b203f854ae src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/Perm.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -335,7 +335,7 @@
 by (rtac lam_funtype 2);
 by (typechk_tac (prem::ZF_typechecks));
 by (asm_simp_tac (!simpset 
-             setsolver type_auto_tac [lam_type, lam_funtype, prem]) 1);
+             setSolver type_auto_tac [lam_type, lam_funtype, prem]) 1);
 qed "comp_lam";
 
 goal Perm.thy "!!f g. [| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
@@ -343,7 +343,7 @@
     f_imp_injective 1);
 by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
 by (asm_simp_tac (!simpset  addsimps [left_inverse] 
-                        setsolver type_auto_tac [inj_is_fun, apply_type]) 1);
+                        setSolver type_auto_tac [inj_is_fun, apply_type]) 1);
 qed "comp_inj";
 
 goalw Perm.thy [surj_def]
@@ -544,7 +544,7 @@
     "!!f. [| f: inj(A,B);  a~:A;  b~:B |]  ==> \
 \         cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
 by (fast_tac (!claset  addIs [apply_type]
-                     addss (!simpset addsimps [fun_extend, fun_extend_apply2,
+              unsafe_addss (!simpset addsimps [fun_extend, fun_extend_apply2,
                                             fun_extend_apply1]) ) 1);
 qed "inj_extend";
 
diff -r 4b30dbe4a020 -r e9b203f854ae src/ZF/WF.ML
--- a/src/ZF/WF.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/WF.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -225,7 +225,7 @@
                         eresolve_tac [underD, transD, spec RS mp]));
 
 (*** NOTE! some simplifications need a different solver!! ***)
-val wf_super_ss = !simpset setsolver indhyp_tac;
+val wf_super_ss = !simpset setSolver indhyp_tac;
 
 val prems = goalw WF.thy [is_recfun_def]
     "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \
diff -r 4b30dbe4a020 -r e9b203f854ae src/ZF/ex/Bin.ML
--- a/src/ZF/ex/Bin.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/ex/Bin.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -379,7 +379,7 @@
               bin_mult_Plus, bin_mult_Minus,
               bin_mult_Bcons1, bin_mult_Bcons0] @
              norm_Bcons_simps
-    setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
+    setSolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
 
 
 (*** Examples of performing binary arithmetic by simplification ***)
diff -r 4b30dbe4a020 -r e9b203f854ae src/ZF/ex/Primrec.ML
--- a/src/ZF/ex/Primrec.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/ex/Primrec.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -22,7 +22,7 @@
 
 (** Useful special cases of evaluation ***)
 
-simpset := !simpset setsolver (type_auto_tac pr_typechecks);
+simpset := !simpset setSolver (type_auto_tac pr_typechecks);
 
 goalw Primrec.thy [SC_def]
     "!!x l. [| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
@@ -61,7 +61,7 @@
 (* c: primrec ==> c: list(nat) -> nat *)
 val primrec_into_fun = primrec.dom_subset RS subsetD;
 
-simpset := !simpset setsolver (type_auto_tac ([primrec_into_fun] @ 
+simpset := !simpset setSolver (type_auto_tac ([primrec_into_fun] @ 
 					      pr_typechecks @ primrec.intrs));
 
 goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
diff -r 4b30dbe4a020 -r e9b203f854ae src/ZF/ex/TF.ML
--- a/src/ZF/ex/TF.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/ex/TF.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -202,7 +202,7 @@
     [TconsI, FnilI, FconsI, treeI, forestI,
      list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
 
-simpset := !simpset setsolver type_auto_tac (list_typechecks@TF_typechecks);
+simpset := !simpset setSolver type_auto_tac (list_typechecks@TF_typechecks);
 
 (** theorems about list_of_TF and TF_of_list **)
 
diff -r 4b30dbe4a020 -r e9b203f854ae src/ZF/ex/Term.ML
--- a/src/ZF/ex/Term.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/ex/Term.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -172,7 +172,7 @@
 (*map_type2 and term_map_type2 instantiate variables*)
 simpset := !simpset
       addsimps [term_rec, term_map, term_size, reflect, preorder]
-      setsolver type_auto_tac (list_typechecks@term_typechecks);
+      setSolver type_auto_tac (list_typechecks@term_typechecks);
 
 
 (** theorems about term_map **)
diff -r 4b30dbe4a020 -r e9b203f854ae src/ZF/indrule.ML
--- a/src/ZF/indrule.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/indrule.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -82,7 +82,7 @@
   fail.  *)
 val min_ss = empty_ss
       setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
-      setsolver  (fn prems => resolve_tac (triv_rls@prems) 
+      setSolver  (fn prems => resolve_tac (triv_rls@prems) 
                               ORELSE' assume_tac
                               ORELSE' etac FalseE);