# HG changeset patch
# User wenzelm
# Date 1205963442 -3600
# Node ID 0f65fa163304b694179e0d2178bb8a38208b3604
# Parent  2f5a4367a39e845912c6b0571f7140e04cd187a9
more antiquotations;

diff -r 2f5a4367a39e -r 0f65fa163304 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/CCL/CCL.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -390,7 +390,7 @@
 local
   fun mk_thm s = prove_goal (the_context ()) s (fn _ =>
                           [rtac notI 1,dtac (thm "case_pocong") 1,etac rev_mp 5,
-                           ALLGOALS (simp_tac (simpset ())),
+                           ALLGOALS (simp_tac @{simpset}),
                            REPEAT (resolve_tac [thm "po_refl", thm "npo_lam_bot"] 1)])
 in
 
diff -r 2f5a4367a39e -r 0f65fa163304 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/CCL/Term.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -209,11 +209,11 @@
 
 fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
            (fn _ => [stac letrecB 1,
-                     simp_tac (simpset () addsimps rawBs) 1]);
+                     simp_tac (@{simpset} addsimps rawBs) 1]);
 fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
 
 fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
-           (fn _ => [simp_tac (simpset () addsimps rawBs
+           (fn _ => [simp_tac (@{simpset} addsimps rawBs
                                setloop (stac letrecB)) 1]);
 fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
 
@@ -298,7 +298,7 @@
 
 local
   fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
-    [simp_tac (simpset () addsimps (thms "ccl_porews")) 1])
+    [simp_tac (@{simpset} addsimps (thms "ccl_porews")) 1])
 in
   val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
                                 "inr(b) [= inr(b') <-> b [= b'",
diff -r 2f5a4367a39e -r 0f65fa163304 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/CCL/Type.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -397,7 +397,7 @@
   val lfpI = thm "lfpI"
   val coinduct3_mono_lemma = thm "coinduct3_mono_lemma"
   fun mk_thm s = prove_goal (the_context ()) s (fn mono::prems =>
-       [fast_tac (claset () addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1])
+       [fast_tac (@{claset} addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1])
 in
 val ci3_RI    = mk_thm "[|  mono(Agen);  a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"
 val ci3_AgenI = mk_thm "[|  mono(Agen);  a : Agen(lfp(%x. Agen(x) Un R Un A)) |] ==> a : lfp(%x. Agen(x) Un R Un A)"
@@ -405,8 +405,8 @@
 
 fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
       (fn prems => [rtac (genXH RS iffD2) 1,
-                    simp_tac (simpset ()) 1,
-                    TRY (fast_tac (claset () addIs
+                    SIMPSET' simp_tac 1,
+                    TRY (fast_tac (@{claset} addIs
                             ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
                              @ prems)) 1)])
 end;
diff -r 2f5a4367a39e -r 0f65fa163304 src/FOL/ex/Classical.thy
--- a/src/FOL/ex/Classical.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/FOL/ex/Classical.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -459,7 +459,7 @@
                   ((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b)))))  
    -->                   
    ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
-by (tactic{*Blast.depth_tac (claset ()) 12 1*})
+by (tactic{*Blast.depth_tac @{claset} 12 1*})
    --{*Needed because the search for depths below 12 is very slow*}
 
 
diff -r 2f5a4367a39e -r 0f65fa163304 src/FOL/ex/Miniscope.thy
--- a/src/FOL/ex/Miniscope.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/FOL/ex/Miniscope.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -65,8 +65,8 @@
 lemmas mini_simps = demorgans nnf_simps ex_simps all_simps
 
 ML {*
-val mini_ss = simpset() addsimps (thms "mini_simps");
-val mini_tac = rtac (thm "ccontr") THEN' asm_full_simp_tac mini_ss;
+val mini_ss = @{simpset} addsimps @{thms mini_simps};
+val mini_tac = rtac @{thm ccontr} THEN' asm_full_simp_tac mini_ss;
 *}
 
 end
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Algebra/abstract/Ideal2.thy
--- a/src/HOL/Algebra/abstract/Ideal2.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Algebra/abstract/Ideal2.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -115,8 +115,8 @@
    apply (rule subsetI)
    apply (drule InterD)
     prefer 2 apply assumption
-   apply (tactic {* auto_tac (claset() addIs [thm "is_ideal_2"],
-     simpset() delsimprocs [ring_simproc]) *})
+   apply (tactic {* auto_tac (@{claset} addIs [@{thm is_ideal_2}],
+     @{simpset} delsimprocs [ring_simproc]) *})
    apply (rule_tac x = "1" in exI)
    apply (rule_tac x = "0" in exI)
    apply (rule_tac [2] x = "0" in exI)
@@ -283,7 +283,7 @@
   apply (drule_tac f = "op* aa" in arg_cong)
   apply (simp add: r_distr)
   apply (erule subst)
-  apply (tactic {* asm_simp_tac (simpset() addsimps [thm "m_assoc" RS sym]
+  apply (tactic {* asm_simp_tac (@{simpset} addsimps [@{thm m_assoc} RS sym]
     delsimprocs [ring_simproc]) 1 *})
   done
 
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -465,7 +465,7 @@
 
 lemma r_inverse_ring: "!! a::'a::ring. a dvd 1 ==> a * inverse a = 1"
   apply (unfold inverse_def dvd_def)
-  apply (tactic {* asm_full_simp_tac (simpset () delsimprocs [ring_simproc]) 1 *})
+  apply (tactic {* asm_full_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
   apply clarify
   apply (rule theI)
    apply assumption
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Algebra/poly/LongDiv.thy
--- a/src/HOL/Algebra/poly/LongDiv.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -129,16 +129,16 @@
   apply (rule_tac x = "((% (q,r,k) . (monom (lcoeff g ^ k * lcoeff x) (deg x - deg g) + q)) xa, (% (q,r,k) . r) xa, (% (q,r,k) . Suc k) xa) " in exI)
   apply clarify
   apply (drule sym)
-  apply (tactic {* simp_tac (simpset() addsimps [thm "l_distr", thm "a_assoc"]
+  apply (tactic {* simp_tac (@{simpset} addsimps [@{thm l_distr}, @{thm a_assoc}]
     delsimprocs [ring_simproc]) 1 *})
-  apply (tactic {* asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1 *})
-  apply (tactic {* simp_tac (simpset () addsimps [thm "minus_def", thm "smult_r_distr",
+  apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
+  apply (tactic {* simp_tac (@{simpset} addsimps [thm "minus_def", thm "smult_r_distr",
     thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc1", thm "smult_assoc2"]
     delsimprocs [ring_simproc]) 1 *})
   apply simp
   done
 
-ML {* simplify (simpset() addsimps [thm "eucl_size_def"]
+ML {* simplify (@{simpset} addsimps [thm "eucl_size_def"]
     delsimprocs [ring_simproc]) (thm "long_div_eucl_size") *}
 
 thm long_div_eucl_size [simplified]
@@ -148,9 +148,9 @@
      Ex (% (q, r, k).  
        (lcoeff g)^k *s f = q * g + r & (r = 0 | deg r < deg g))"
   apply (tactic {* forw_inst_tac [("f", "f")]
-    (simplify (simpset() addsimps [thm "eucl_size_def"]
+    (simplify (@{simpset} addsimps [thm "eucl_size_def"]
       delsimprocs [ring_simproc]) (thm "long_div_eucl_size")) 1 *})
-  apply (tactic {* auto_tac (claset(), simpset() delsimprocs [ring_simproc]) *})
+  apply (tactic {* auto_tac (@{claset}, @{simpset} delsimprocs [ring_simproc]) *})
   apply (case_tac "aa = 0")
    apply blast
   (* case "aa ~= 0 *)
@@ -169,7 +169,7 @@
   apply (rule conjI)
    apply (drule sym)
    apply (tactic {* asm_simp_tac
-     (simpset() addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"]
+     (@{simpset} addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"]
      delsimprocs [ring_simproc]) 1 *})
    apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric])
   (* degree property *)
@@ -194,7 +194,7 @@
 
 lemma diff_zero_imp_eq: "!!a::'a::ring. a - b = 0 ==> a = b"
   apply (rule_tac s = "a - (a - b) " in trans)
-   apply (tactic {* asm_simp_tac (simpset() delsimprocs [ring_simproc]) 1 *})
+   apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
    apply simp
   apply (simp (no_asm))
   done
@@ -215,22 +215,22 @@
   (* r1 = 0 *)
     apply (erule disjE)
   (* r2 = 0 *)
-     apply (tactic {* asm_full_simp_tac (simpset()
+     apply (tactic {* asm_full_simp_tac (@{simpset}
        addsimps [thm "integral_iff", thm "minus_def", thm "l_zero", thm "uminus_zero"]
        delsimprocs [ring_simproc]) 1 *})
   (* r2 ~= 0 *)
     apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
-    apply (tactic {* asm_full_simp_tac (simpset() addsimps
+    apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
       [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
   (* r1 ~=0 *)
    apply (erule disjE)
   (* r2 = 0 *)
     apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
-    apply (tactic {* asm_full_simp_tac (simpset() addsimps
+    apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
       [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
   (* r2 ~= 0 *)
    apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
-   apply (tactic {* asm_full_simp_tac (simpset() addsimps [thm "minus_def"]
+   apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [thm "minus_def"]
      delsimprocs [ring_simproc]) 1 *})
    apply (drule order_eq_refl [THEN add_leD2])
    apply (drule leD)
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Auth/Message.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -847,8 +847,8 @@
   concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
   alone.*)
 fun prove_simple_subgoals_tac i = 
-    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
-    ALLGOALS Asm_simp_tac
+    CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
+    ALLGOALS (SIMPSET' asm_simp_tac)
 
 (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   but this application is no longer necessary if analz_insert_eq is used.
@@ -886,7 +886,7 @@
        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
        DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
 
-fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
+val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
 
 end
 *}
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Bali/AxExample.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -136,7 +136,7 @@
 apply       (rule ax_subst_Var_allI)
 apply       (tactic {* inst1_tac "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
 apply       (rule allI)
-apply       (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
+apply       (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
 apply       (rule ax_derivs.Abrupt)
 apply      (simp (no_asm))
 apply      (tactic "ax_tac 1" (* FVar *))
@@ -186,26 +186,26 @@
 apply  (rule ax_InitS)
 apply     force
 apply    (simp (no_asm))
-apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
+apply   (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
 apply   (rule ax_Init_Skip_lemma)
-apply  (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
+apply  (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
 apply  (rule ax_InitS [THEN conseq1] (* init Base *))
 apply      force
 apply     (simp (no_asm))
 apply    (unfold arr_viewed_from_def)
 apply    (rule allI)
 apply    (rule_tac P' = "Normal ?P" in conseq1)
-apply     (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
+apply     (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
 apply     (tactic "ax_tac 1")
 apply     (tactic "ax_tac 1")
 apply     (rule_tac [2] ax_subst_Var_allI)
 apply      (tactic {* inst1_tac "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
-apply     (tactic {* simp_tac (simpset() delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
+apply     (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
 apply      (tactic "ax_tac 2" (* NewA *))
 apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
 apply       (tactic "ax_tac 3")
 apply      (tactic {* inst1_tac "P" "\<lambda>vf l vfa. Normal (?P vf l vfa\<leftarrow>\<diamondsuit>)" *})
-apply      (tactic {* simp_tac (simpset() delloop "split_all_tac") 2 *})
+apply      (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 2 *})
 apply      (tactic "ax_tac 2")
 apply     (tactic "ax_tac 1" (* FVar *))
 apply      (tactic "ax_tac 2" (* StatRef *))
@@ -216,7 +216,7 @@
 apply     (drule initedD)
 apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
 apply    force
-apply   (tactic {* simp_tac (simpset() delloop "split_all_tac") 1 *})
+apply   (tactic {* simp_tac (@{simpset} delloop "split_all_tac") 1 *})
 apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
 apply     (rule wf_tprg)
 apply    clarsimp
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Bali/AxSem.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -699,7 +699,7 @@
 (*42 subgoals*)
 apply       (tactic "ALLGOALS strip_tac")
 apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
-         etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})
+         etac disjE, fast_tac (@{claset} addSIs [thm "ax_derivs.empty"])]))*})
 apply       (tactic "TRYALL hyp_subst_tac")
 apply       (simp, rule ax_derivs.empty)
 apply      (drule subset_insertD)
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Bali/Example.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -1193,7 +1193,7 @@
         Base_foo_defs  [simp]
 
 ML_setup {* bind_thms ("eval_intros", map 
-        (simplify (simpset() delsimps @{thms Skip_eq}
+        (simplify (@{simpset} delsimps @{thms Skip_eq}
                              addsimps @{thms lvar_def}) o 
          rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
 lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Fun.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -532,7 +532,7 @@
 subsection {* ML legacy bindings *} 
 
 ML {*
-val set_cs = claset() delrules [equalityI]
+val set_cs = @{claset} delrules [@{thm equalityI}]
 *}
 
 ML {*
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/HoareParallel/Gar_Coll.thy
--- a/src/HOL/HoareParallel/Gar_Coll.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/HoareParallel/Gar_Coll.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -796,9 +796,9 @@
 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
 apply(tactic {* TRYALL (etac disjE) *})
 apply simp_all
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{clasimpset}]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
 done
 
 subsubsection {* Interference freedom Mutator-Collector *}
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/HoareParallel/Mul_Gar_Coll.thy
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -1200,7 +1200,7 @@
 --{* 72 subgoals left *}
 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
 --{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac (thm "Graph3"),force_tac (clasimpset ()), assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
 --{* 28 subgoals left *}
 apply(tactic {* TRYALL (etac conjE) *})
 apply(tactic {* TRYALL (etac disjE) *})
@@ -1210,17 +1210,17 @@
 apply(tactic {* ALLGOALS(case_tac "M x!(T (Muts x ! j))=Black") *})
 apply(simp_all add:Graph10)
 --{* 47 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
 --{* 41 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (claset(),simpset() addsimps [thm "Queue_def", @{thm less_Suc_eq_le}, thm "le_length_filter_update"])]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
 --{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac @{clasimpset}]) *})
 --{* 31 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
 --{* 29 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac (clasimpset ())]) *})
+apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
 --{* 25 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (claset(),simpset() addsimps [thm "Queue_def", @{thm less_Suc_eq_le}, thm "le_length_filter_update"])]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
 --{* 10 subgoals left *}
 apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+
 done
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/IMP/VC.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -77,7 +77,7 @@
   apply fast
  (* if *)
  apply atomize
- apply (tactic "Deepen_tac 4 1")
+ apply (tactic "deepen_tac @{claset} 4 1")
 (* while *)
 apply atomize
 apply (intro allI impI)
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/IOA/Solve.thy
--- a/src/HOL/IOA/Solve.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/IOA/Solve.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -149,7 +149,7 @@
   apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if)
   apply (tactic {*
     REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
-      asm_full_simp_tac(simpset() addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *})
+      asm_full_simp_tac(@{simpset} addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *})
   done
 
 
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -343,7 +343,7 @@
 apply(rule hconfI)
 apply(drule conforms_heapD)
 apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] 
-                addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *})
+                addDs [thm "hconfD"], @{simpset} delsimps [split_paired_All]) *})
 done
 
 lemma conforms_upd_local: 
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Modelcheck/EindhovenSyn.thy
--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -72,7 +72,7 @@
   (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
 
 val Eindhoven_ss =
-  simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
+  @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
 
 (*check if user has pmu installed*)
 fun eindhoven_enabled () = getenv "EINDHOVEN_HOME" <> "";
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -221,7 +221,7 @@
   Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
   (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
 
-val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
+val Mucke_ss = @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
 
 
 (* the interface *)
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Mar 19 22:50:42 2008 +0100
@@ -111,7 +111,7 @@
 (
 OldGoals.push_proof();
 OldGoals.goalw_cterm [] (cterm_of sign trm);
-by (simp_tac (simpset()) 1);
+by (SIMPSET' simp_tac 1);
         let
         val if_tmp_result = result()
         in
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/NatBin.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -625,7 +625,7 @@
 
 ML
 {*
-val numeral_ss = simpset() addsimps @{thms numerals};
+val numeral_ss = @{simpset} addsimps @{thms numerals};
 
 val nat_bin_arith_setup =
  LinArith.map_data
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -386,9 +386,11 @@
   and   "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>y"
   by (simp_all add: fresh_prod)
 
-ML_setup {*
-  val mksimps_pairs = ("Nominal.fresh", thms "fresh_prodD")::mksimps_pairs;
-  change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
+ML {*
+  val mksimps_pairs = (@{const_name Nominal.fresh}, @{thms fresh_prodD}) :: mksimps_pairs;
+*}
+declaration {* fn _ =>
+  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
 *}
 
 
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/SET-Protocol/MessageSET.thy
--- a/src/HOL/SET-Protocol/MessageSET.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -844,8 +844,8 @@
   concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
   alone.*)
 fun prove_simple_subgoals_tac i =
-    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
-    ALLGOALS Asm_simp_tac
+    CLASIMPSET' (fn (cs, ss) => force_tac (cs, ss addsimps [@{thm image_eq_UN}])) i THEN
+    ALLGOALS (SIMPSET' asm_simp_tac)
 
 (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   but this application is no longer necessary if analz_insert_eq is used.
@@ -883,7 +883,7 @@
        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
        DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
 
-fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
+val spy_analz_tac = CLASIMPSET' gen_spy_analz_tac;
 
 end
 *}
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/TLA/Buffer/DBuffer.thy
--- a/src/HOL/TLA/Buffer/DBuffer.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Buffer/DBuffer.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -63,7 +63,7 @@
   apply (rule square_simulation)
    apply clarsimp
   apply (tactic
-    {* action_simp_tac (simpset () addsimps (thm "hd_append" :: thms "db_defs")) [] [] 1 *})
+    {* action_simp_tac (@{simpset} addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1 *})
   done
 
 
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/TLA/Inc/Inc.thy
--- a/src/HOL/TLA/Inc/Inc.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Inc/Inc.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -115,7 +115,7 @@
   by (auto simp: PsiInv_defs)
 
 lemma PsiInv: "|- Psi --> []PsiInv"
-  apply (tactic {* inv_tac (clasimpset () addsimps2 [thm "Psi_def"]) 1 *})
+  apply (tactic {* inv_tac (@{clasimpset} addsimps2 [@{thm Psi_def}]) 1 *})
    apply (force simp: PsiInv_Init [try_rewrite] Init_def)
   apply (auto intro: PsiInv_alpha1 [try_rewrite] PsiInv_alpha2 [try_rewrite]
     PsiInv_beta1 [try_rewrite] PsiInv_beta2 [try_rewrite] PsiInv_gamma1 [try_rewrite]
@@ -128,7 +128,7 @@
 *)
 
 lemma "|- Psi --> []PsiInv"
-  by (tactic {* auto_inv_tac (simpset() addsimps (thms "PsiInv_defs" @ thms "Psi_defs")) 1 *})
+  by (tactic {* auto_inv_tac (@{simpset} addsimps (@{thms PsiInv_defs} @ @{thms Psi_defs})) 1 *})
 
 
 (**** Step simulation ****)
@@ -174,9 +174,9 @@
     --> (pc1 = #g ~> pc1 = #a)"
   apply (rule SF1)
     apply (tactic
-      {* action_simp_tac (simpset () addsimps (thms "Psi_defs")) [] [thm "squareE"] 1 *})
+      {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
    apply (tactic
-      {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs")) [] [] 1 *})
+      {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
   (* reduce |- []A --> <>Enabled B  to  |- A --> Enabled B *)
   apply (auto intro!: InitDmd_gen [temp_use] N1_enabled_at_g [temp_use]
     dest!: STL2_gen [temp_use] simp: Init_def)
@@ -195,8 +195,8 @@
   "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True  
     --> (pc2 = #g ~> pc2 = #a)"
   apply (rule SF1)
-  apply (tactic {* action_simp_tac (simpset () addsimps (thms "Psi_defs")) [] [thm "squareE"] 1 *})
-  apply (tactic {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs"))
+  apply (tactic {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
+  apply (tactic {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs})
     [] [] 1 *})
   apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_g [temp_use]
     dest!: STL2_gen [temp_use] simp add: Init_def)
@@ -215,9 +215,9 @@
     --> (pc2 = #b ~> pc2 = #g)"
   apply (rule SF1)
     apply (tactic
-      {* action_simp_tac (simpset () addsimps (thms "Psi_defs")) [] [thm "squareE"] 1 *})
+      {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
    apply (tactic
-     {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs")) [] [] 1 *})
+     {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
   apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_b [temp_use]
     dest!: STL2_gen [temp_use] simp: Init_def)
   done
@@ -257,9 +257,9 @@
          & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)   
          --> (pc1 = #a ~> pc1 = #b)"
   apply (rule SF1)
-  apply (tactic {* action_simp_tac (simpset () addsimps thms "Psi_defs") [] [thm "squareE"] 1 *})
+  apply (tactic {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
   apply (tactic
-    {* action_simp_tac (simpset () addsimps (thm "angle_def" :: thms "Psi_defs")) [] [] 1 *})
+    {* action_simp_tac (@{simpset} addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1 *})
   apply (clarsimp intro!: N1_enabled_at_both_a [THEN DmdImpl [temp_use]])
   apply (auto intro!: BoxDmd2_simple [temp_use] N2_live [temp_use]
     simp: split_box_conj more_temp_simps)
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/TLA/Memory/MemClerk.thy
--- a/src/HOL/TLA/Memory/MemClerk.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -84,7 +84,7 @@
 lemma MClkFwd_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
       |- Calling send p & ~Calling rcv p & cst!p = #clkA   
          --> Enabled (MClkFwd send rcv cst p)"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "MClkFwd_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
     thm "Call_def", thm "caller_def", thm "rtrner_def"]) [exI]
     [thm "base_enabled", Pair_inject] 1 *})
 
@@ -99,9 +99,9 @@
 lemma MClkReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, cst!p) ==>  
       |- Calling send p & ~Calling rcv p & cst!p = #clkB   
          --> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
-  apply (tactic {* action_simp_tac (simpset ())
+  apply (tactic {* action_simp_tac @{simpset}
     [thm "MClkReply_change" RSN (2, thm "enabled_mono") ] [] 1 *})
-  apply (tactic {* action_simp_tac (simpset () addsimps
+  apply (tactic {* action_simp_tac (@{simpset} addsimps
     [thm "MClkReply_def", thm "Return_def", thm "caller_def", thm "rtrner_def"])
     [exI] [thm "base_enabled", Pair_inject] 1 *})
   done
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/TLA/Memory/Memory.thy
--- a/src/HOL/TLA/Memory/Memory.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Memory/Memory.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -152,7 +152,7 @@
 (* The memory spec implies the memory invariant *)
 lemma MemoryInvariant: "|- MSpec ch mm rs l --> [](MemInv mm l)"
   by (tactic {* auto_inv_tac
-    (simpset () addsimps (thms "RM_temp_defs" @ thms "RM_action_defs")) 1 *})
+    (@{simpset} addsimps (@{thms RM_temp_defs} @ @{thms RM_action_defs})) 1 *})
 
 (* The invariant is trivial for non-locations *)
 lemma NonMemLocInvariant: "|- #l ~: #MemLoc --> [](MemInv mm l)"
@@ -182,9 +182,9 @@
       |- Calling ch p & (rs!p ~= #NotAResult)
          --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
   apply (tactic
-    {* action_simp_tac (simpset ()) [thm "MemReturn_change" RSN (2, thm "enabled_mono") ] [] 1 *})
+    {* action_simp_tac @{simpset} [thm "MemReturn_change" RSN (2, thm "enabled_mono") ] [] 1 *})
   apply (tactic
-    {* action_simp_tac (simpset () addsimps [thm "MemReturn_def", thm "Return_def",
+    {* action_simp_tac (@{simpset} addsimps [thm "MemReturn_def", thm "Return_def",
       thm "rtrner_def"]) [exI] [thm "base_enabled", thm "Pair_inject"] 1 *})
   done
 
@@ -228,11 +228,11 @@
          --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
   apply (case_tac "arg (ch w p)")
-   apply (tactic {* action_simp_tac (simpset () addsimps [thm "Read_def",
+   apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Read_def",
      temp_rewrite (thm "enabled_ex")]) [thm "ReadInner_enabled", exI] [] 1 *})
    apply (force dest: base_pair [temp_use])
   apply (erule contrapos_np)
-  apply (tactic {* action_simp_tac (simpset () addsimps [thm "Write_def",
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Write_def",
     temp_rewrite (thm "enabled_ex")])
     [thm "WriteInner_enabled", exI] [] 1 *})
   done
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -220,9 +220,9 @@
   apply (rule historyI)
       apply assumption+
   apply (rule MI_base)
-  apply (tactic {* action_simp_tac (simpset () addsimps [thm "HInit_def"]) [] [] 1 *})
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HInit_def"]) [] [] 1 *})
    apply (erule fun_cong)
-  apply (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def"])
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def"])
     [thm "busy_squareI"] [] 1 *})
   apply (erule fun_cong)
   done
@@ -324,7 +324,7 @@
 
 lemma S1Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
          --> unchanged (rmhist!p)"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def", thm "S_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", thm "S_def",
     thm "S1_def", thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def",
     thm "Return_def"]) [] [temp_use (thm "squareE")] 1 *})
 
@@ -340,7 +340,7 @@
 lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p
          & unchanged (e p, r p, m p, rmhist!p)
          --> (S3 rmhist p)$"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "MClkFwd_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
     thm "Call_def", thm "e_def", thm "r_def", thm "m_def", thm "caller_def",
     thm "rtrner_def", thm "S_def", thm "S2_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
 
@@ -376,7 +376,7 @@
 lemma S3Forward: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
          & unchanged (e p, c p, m p)
          --> (S4 rmhist p)$ & unchanged (rmhist!p)"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCFwd_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFwd_def",
     thm "HNext_def", thm "MemReturn_def", thm "RPCFail_def",
     thm "MClkReply_def", thm "Return_def", thm "Call_def", thm "e_def",
     thm "c_def", thm "m_def", thm "caller_def", thm "rtrner_def", thm "S_def",
@@ -385,7 +385,7 @@
 lemma S3Fail: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
          & unchanged (e p, c p, m p)
          --> (S6 rmhist p)$"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
     thm "RPCFail_def", thm "Return_def", thm "e_def", thm "c_def",
     thm "m_def", thm "caller_def", thm "rtrner_def", thm "MVOKBARF_def",
     thm "S_def", thm "S3_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
@@ -412,7 +412,7 @@
 lemma S4ReadInner: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
          & HNext rmhist p & $(MemInv mm l)
          --> (S4 rmhist p)$ & unchanged (rmhist!p)"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "ReadInner_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
     thm "GoodRead_def", thm "BadRead_def", thm "HNext_def", thm "MemReturn_def",
     thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
     thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def",
@@ -426,7 +426,7 @@
 
 lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p)           & HNext rmhist p
          --> (S4 rmhist p)$ & unchanged (rmhist!p)"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "WriteInner_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "WriteInner_def",
     thm "GoodWrite_def", thm "BadWrite_def", thm "HNext_def", thm "MemReturn_def",
     thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
     thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def", thm "MVNROKBA_def",
@@ -465,14 +465,14 @@
 
 lemma S5Reply: "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
        --> (S6 rmhist p)$"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCReply_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
     thm "Return_def", thm "e_def", thm "c_def", thm "m_def", thm "MVOKBA_def",
     thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def", thm "S_def",
     thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
 
 lemma S5Fail: "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
          --> (S6 rmhist p)$"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCFail_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
     thm "Return_def", thm "e_def", thm "c_def", thm "m_def",
     thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def",
     thm "S_def", thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
@@ -498,7 +498,7 @@
 lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
          & unchanged (e p,r p,m p)
          --> (S3 rmhist p)$ & unchanged (rmhist!p)"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
     thm "MClkReply_def", thm "MClkRetry_def", thm "Call_def", thm "Return_def",
     thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
     thm "S_def", thm "S6_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
@@ -506,7 +506,7 @@
 lemma S6Reply: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
          & unchanged (e p,r p,m p)
          --> (S1 rmhist p)$"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "HNext_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
     thm "MemReturn_def", thm "RPCFail_def", thm "Return_def", thm "MClkReply_def",
     thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
     thm "S_def", thm "S6_def", thm "S1_def", thm "Calling_def"]) [] [] 1 *})
@@ -538,7 +538,7 @@
 lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
          & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
          --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
-  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
       (map temp_elim [thm "S1ClerkUnch", thm "S1RPCUnch", thm "S1MemUnch", thm "S1Hist"]) 1 *})
    apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S1Env")]) *})
   done
@@ -547,7 +547,7 @@
          & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
          --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
              & unchanged (e p, r p, m p, rmhist!p)"
-  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
     (map temp_elim [thm "S2EnvUnch", thm "S2RPCUnch", thm "S2MemUnch", thm "S2Hist"]) 1 *})
    apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S2Clerk"),
      temp_use (thm "S2Forward")]) *})
@@ -557,9 +557,9 @@
          & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
          --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
              | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
-  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
     (map temp_elim [thm "S3EnvUnch", thm "S3ClerkUnch", thm "S3MemUnch"]) 1 *})
-  apply (tactic {* action_simp_tac (simpset()) []
+  apply (tactic {* action_simp_tac @{simpset} []
     (thm "squareE" :: map temp_elim [thm "S3RPC", thm "S3Forward", thm "S3Fail"]) 1 *})
    apply (auto dest!: S3Hist [temp_use])
   done
@@ -570,9 +570,9 @@
          --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
              | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
              | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
-  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
     (map temp_elim [thm "S4EnvUnch", thm "S4ClerkUnch", thm "S4RPCUnch"]) 1 *})
-  apply (tactic {* action_simp_tac (simpset() addsimps [thm "RNext_def"]) []
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "RNext_def"]) []
     (thm "squareE" :: map temp_elim [thm "S4Read", thm "S4Write", thm "S4Return"]) 1 *})
   apply (auto dest!: S4Hist [temp_use])
   done
@@ -581,9 +581,9 @@
               & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
          --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
              | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
-  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
     (map temp_elim [thm "S5EnvUnch", thm "S5ClerkUnch", thm "S5MemUnch", thm "S5Hist"]) 1 *})
-  apply (tactic {* action_simp_tac (simpset()) [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
+  apply (tactic {* action_simp_tac @{simpset} [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
    apply (tactic {* auto_tac (MI_fast_css addSDs2
      [temp_use (thm "S5Reply"), temp_use (thm "S5Fail")]) *})
   done
@@ -592,9 +592,9 @@
               & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
          --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
              | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
-  apply (tactic {* action_simp_tac (simpset() addsimps [thm "ImpNext_def"]) []
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
     (map temp_elim [thm "S6EnvUnch", thm "S6RPCUnch", thm "S6MemUnch"]) 1 *})
-  apply (tactic {* action_simp_tac (simpset()) []
+  apply (tactic {* action_simp_tac @{simpset} []
     (thm "squareE" :: map temp_elim [thm "S6Clerk", thm "S6Retry", thm "S6Reply"]) 1 *})
      apply (auto dest: S6Hist [temp_use])
   done
@@ -606,7 +606,7 @@
 section "Initialization (Step 1.3)"
 
 lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "resbar_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "resbar_def",
     thm "PInit_def", thm "S_def", thm "S1_def"]) [] [] 1 *})
 
 (* ----------------------------------------------------------------------
@@ -625,7 +625,7 @@
          & unchanged (e p, r p, m p, rmhist!p)
          --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   by (tactic {* action_simp_tac
-    (simpset() addsimps [thm "MClkFwd_def", thm "e_def", thm "r_def", thm "m_def",
+    (@{simpset} addsimps [thm "MClkFwd_def", thm "e_def", thm "r_def", thm "m_def",
     thm "resbar_def", thm "S_def", thm "S2_def", thm "S3_def"]) [] [] 1 *})
 
 lemma Step1_4_3a: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
@@ -633,7 +633,7 @@
          --> unchanged (rtrner memCh!p, resbar rmhist!p)"
   apply clarsimp
   apply (drule S3_excl [temp_use] S4_excl [temp_use])+
-  apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def",
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
     thm "c_def", thm "m_def", thm "resbar_def", thm "S_def", thm "S3_def"]) [] [] 1 *})
   done
 
@@ -652,11 +652,11 @@
          --> ReadInner memCh mm (resbar rmhist) p l"
   apply clarsimp
   apply (drule S4_excl [temp_use])+
-  apply (tactic {* action_simp_tac (simpset () addsimps [thm "ReadInner_def",
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
     thm "GoodRead_def", thm "BadRead_def", thm "e_def", thm "c_def", thm "m_def"]) [] [] 1 *})
      apply (auto simp: resbar_def)
        apply (tactic {* ALLGOALS (action_simp_tac
-                (simpset() addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def",
+                (@{simpset} addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def",
                   thm "S_def", thm "S4_def", thm "RdRequest_def", thm "MemInv_def"])
                 [] [thm "impE", thm "MemValNotAResultE"]) *})
   done
@@ -671,11 +671,11 @@
          --> WriteInner memCh mm (resbar rmhist) p l v"
   apply clarsimp
   apply (drule S4_excl [temp_use])+
-  apply (tactic {* action_simp_tac (simpset () addsimps
+  apply (tactic {* action_simp_tac (@{simpset} addsimps
     [thm "WriteInner_def", thm "GoodWrite_def", thm "BadWrite_def", thm "e_def",
     thm "c_def", thm "m_def"]) [] [] 1 *})
      apply (auto simp: resbar_def)
-    apply (tactic {* ALLGOALS (action_simp_tac (simpset () addsimps
+    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
       [thm "RPCRelayArg_def", thm "MClkRelayArg_def", thm "S_def",
       thm "S4_def", thm "WrRequest_def"]) [] []) *})
   done
@@ -688,7 +688,7 @@
 lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
          & unchanged (e p, c p, r p)
          --> unchanged (rtrner memCh!p, resbar rmhist!p)"
-  apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def",
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
     thm "c_def", thm "r_def", thm "resbar_def"]) [] [] 1 *})
   apply (drule S4_excl [temp_use] S5_excl [temp_use])+
   apply (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MemReturn_def", thm "Return_def"]) *})
@@ -717,11 +717,11 @@
          --> MemReturn memCh (resbar rmhist) p"
   apply clarsimp
   apply (drule S6_excl [temp_use])+
-  apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def",
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
     thm "r_def", thm "m_def", thm "MClkReply_def", thm "MemReturn_def",
     thm "Return_def", thm "resbar_def"]) [] [] 1 *})
     apply simp_all (* simplify if-then-else *)
-    apply (tactic {* ALLGOALS (action_simp_tac (simpset () addsimps
+    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
       [thm "MClkReplyVal_def", thm "S6_def", thm "S_def"]) [] [thm "MVOKBARFnotNR"]) *})
   done
 
@@ -730,7 +730,7 @@
          --> MemFail memCh (resbar rmhist) p"
   apply clarsimp
   apply (drule S3_excl [temp_use])+
-  apply (tactic {* action_simp_tac (simpset () addsimps [thm "e_def", thm "r_def",
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", thm "r_def",
     thm "m_def", thm "MClkRetry_def", thm "MemFail_def", thm "resbar_def"]) [] [] 1 *})
    apply (auto simp: S6_def S_def)
   done
@@ -862,14 +862,14 @@
 
 lemma S1_RNextdisabled: "|- S1 rmhist p -->
          ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
-  apply (tactic {* action_simp_tac (simpset () addsimps [thm "angle_def",
+  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
     thm "S_def", thm "S1_def"]) [notI] [thm "enabledE", temp_elim (thm "Memoryidle")] 1 *})
   apply force
   done
 
 lemma S1_Returndisabled: "|- S1 rmhist p -->
          ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "angle_def", thm "MemReturn_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def", thm "MemReturn_def",
     thm "Return_def", thm "S_def", thm "S1_def"]) [notI] [thm "enabledE"] 1 *})
 
 lemma RNext_fair: "|- []<>S1 rmhist p
@@ -1048,7 +1048,7 @@
 
 lemma MClkReplyS6:
   "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "angle_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
     thm "MClkReply_def", thm "Return_def", thm "ImpInv_def", thm "S_def",
     thm "S1_def", thm "S2_def", thm "S3_def", thm "S4_def", thm "S5_def"]) [] [] 1 *})
 
@@ -1056,7 +1056,7 @@
   apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
      apply (cut_tac MI_base)
      apply (blast dest: base_pair)
-    apply (tactic {* ALLGOALS (action_simp_tac (simpset ()
+    apply (tactic {* ALLGOALS (action_simp_tac (@{simpset}
       addsimps [thm "S_def", thm "S6_def"]) [] []) *})
   done
 
@@ -1067,7 +1067,7 @@
   apply (subgoal_tac "sigma |= []<> (<MClkReply memCh crCh cst p>_ (c p))")
    apply (erule InfiniteEnsures)
     apply assumption
-   apply (tactic {* action_simp_tac (simpset()) []
+   apply (tactic {* action_simp_tac @{simpset} []
      (map temp_elim [thm "MClkReplyS6", thm "S6MClkReply_successors"]) 1 *})
   apply (auto simp: SF_def)
   apply (erule contrapos_np)
@@ -1154,7 +1154,7 @@
          sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
       ==> sigma |= []<>S1 rmhist p"
   apply (rule classical)
-  apply (tactic {* asm_lr_simp_tac (simpset() addsimps
+  apply (tactic {* asm_lr_simp_tac (@{simpset} addsimps
     [temp_use (thm "NotBox"), temp_rewrite (thm "NotDmd")]) 1 *})
   apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
   done
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/TLA/Memory/RPC.thy
--- a/src/HOL/TLA/Memory/RPC.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -103,14 +103,14 @@
 (* Enabledness of some actions *)
 lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
     |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCFail_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
     thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI]
     [thm "base_enabled", thm "Pair_inject"] 1 *})
 
 lemma RPCReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
       |- ~Calling rcv p & Calling send p & rst!p = #rpcB  
          --> Enabled (RPCReply send rcv rst p)"
-  by (tactic {* action_simp_tac (simpset () addsimps [thm "RPCReply_def",
+  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
     thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI]
     [thm "base_enabled", thm "Pair_inject"] 1 *})
 
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOL/W0/W0.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -196,15 +196,15 @@
   apply (unfold new_tv_def)
   apply (tactic "safe_tac HOL_cs")
   -- {* @{text \<Longrightarrow>} *}
-    apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (simpset()
+    apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (@{simpset}
       addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
    apply (subgoal_tac "m \<in> cod s \<or> s l = TVar l")
     apply (tactic "safe_tac HOL_cs")
-     apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (simpset()
+     apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (@{simpset}
        addsimps [thm "free_tv_subst"])) 1 *})
     apply (drule_tac P = "\<lambda>x. m \<in> free_tv x" in subst, assumption)
     apply simp
-   apply (tactic {* fast_tac (set_cs addss (simpset()
+   apply (tactic {* fast_tac (set_cs addss (@{simpset}
      addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *})
   -- {* @{text \<Longleftarrow>} *}
   apply (unfold free_tv_subst cod_def dom_def)
@@ -350,7 +350,7 @@
   apply (tactic {*
     fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
     thm "free_tv_subst_var" RS subsetD]
-    addss (simpset() delsimps (thms "bex_simps")
+    addss (@{simpset} delsimps (thms "bex_simps")
     addsimps [thm "cod_def", thm "dom_def"])) 1 *})
   done
 
@@ -555,7 +555,7 @@
       new_tv_le)
    apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
      addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
-     addss (simpset())) 1 *})
+     addss @{simpset}) 1 *})
   apply (rule lessI [THEN new_tv_subst_var])
   apply (erule sym [THEN mgu_new])
     apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
@@ -563,7 +563,7 @@
         lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le)
   apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
     addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
-    addss (simpset())) 1 *})
+    addss @{simpset}) 1 *})
   done
 
 lemma free_tv_W: "!!n a s t m v. \<W> e a n = Ok (s, t, m) \<Longrightarrow>
@@ -616,7 +616,7 @@
     thm "free_tv_subst_var" RS subsetD,
     thm "free_tv_app_subst_te" RS subsetD,
     thm "free_tv_app_subst_tel" RS subsetD, @{thm less_le_trans}, subsetD]
-    addSEs [UnE] addss (simpset() setSolver unsafe_solver)) 1 *})
+    addSEs [UnE] addss (@{simpset} setSolver unsafe_solver)) 1 *})
       -- {* builtin arithmetic in simpset messes things up *}
   done
 
@@ -798,7 +798,7 @@
     apply (simp add: app_subst_list split: split_if)
    txt {* case @{text "Abs e"} *}
    apply (tactic {* asm_full_simp_tac
-     (simpset() setloop (split_inside_tac [thm "split_bind"])) 1 *})
+     (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *})
    apply (intro strip)
    apply (rule conjI)
     apply (intro strip)
@@ -814,7 +814,7 @@
    apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
      thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *})
   txt {* case @{text "App e1 e2"} *}
-  apply (tactic {* simp_tac (simpset () setloop (split_inside_tac [thm "split_bind"])) 1 *})
+  apply (tactic {* simp_tac (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *})
   apply (intro strip)
   apply (rename_tac s1' t1 n1 s2' t2 n2 sa)
   apply (rule conjI)
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOLCF/IOA/ABP/Correctness.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOLCF/IOA/ABP/Correctness.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -82,7 +82,7 @@
 lemma last_ind_on_first:
     "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
   apply simp
-  apply (tactic {* auto_tac (claset(),
+  apply (tactic {* auto_tac (@{claset},
     HOL_ss addsplits [thm"list.split"]
     addsimps (thms "reverse.simps" @ [thm "hd_append", thm "rev_red_not_nil"])) *})
   done
diff -r 2f5a4367a39e -r 0f65fa163304 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Mar 19 22:50:42 2008 +0100
@@ -6,7 +6,7 @@
 Proof generator for domain command.
 *)
 
-val HOLCF_ss = simpset();
+val HOLCF_ss = @{simpset};
 
 structure Domain_Theorems = struct
 
@@ -113,7 +113,7 @@
 
 val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y" 
   (fn prems =>
-    [blast_tac (claset () addDs [antisym_less_inverse]) 1]);
+    [blast_tac (@{claset} addDs [antisym_less_inverse]) 1]);
 
 in
 
@@ -638,7 +638,7 @@
 (* ----- theorems concerning finite approximation and finite induction ------ *)
 
 local
-  val iterate_Cprod_ss = simpset_of (theory "Fix");
+  val iterate_Cprod_ss = simpset_of @{theory Fix};
   val copy_con_rews  = copy_rews @ con_rews;
   val copy_take_defs =
     (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;