diff -r 40a1865ab122 -r c3d1590debd8 src/HOL/IMPP/Hoare.thy
--- a/src/HOL/IMPP/Hoare.thy	Fri Mar 20 11:26:59 2009 +0100
+++ b/src/HOL/IMPP/Hoare.thy	Fri Mar 20 15:24:18 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/IMPP/Hoare.thy
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 TUM
 *)
@@ -219,7 +218,7 @@
 apply           (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
 prefer 7
 apply          (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
-apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW CLASET' fast_tac) *})
+apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW (fast_tac @{claset})) *})
 done
 
 lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
@@ -291,7 +290,7 @@
    simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
 apply       (simp_all (no_asm_use) add: triple_valid_def2)
 apply       (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
-apply      (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *}) (* Skip, Ass, Local *)
+apply      (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *}) (* Skip, Ass, Local *)
 prefer 3 apply   (force) (* Call *)
 apply  (erule_tac [2] evaln_elim_cases) (* If *)
 apply   blast+
@@ -336,17 +335,17 @@
 lemma MGF_lemma1 [rule_format (no_asm)]: "state_not_singleton ==>  
   !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"
 apply (induct_tac c)
-apply        (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
+apply        (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
 prefer 7 apply        (fast intro: domI)
 apply (erule_tac [6] MGT_alternD)
 apply       (unfold MGT_def)
 apply       (drule_tac [7] bspec, erule_tac [7] domI)
-apply       (rule_tac [7] escape, tactic {* CLASIMPSET' clarsimp_tac 7 *},
+apply       (rule_tac [7] escape, tactic {* clarsimp_tac @{clasimpset} 7 *},
   rule_tac [7] P1 = "%Z' s. s= (setlocs Z newlocs) [Loc Arg ::= fun Z]" in hoare_derivs.Call [THEN conseq1], erule_tac [7] conseq12)
 apply        (erule_tac [!] thin_rl)
 apply (rule hoare_derivs.Skip [THEN conseq2])
 apply (rule_tac [2] hoare_derivs.Ass [THEN conseq1])
-apply        (rule_tac [3] escape, tactic {* CLASIMPSET' clarsimp_tac 3 *},
+apply        (rule_tac [3] escape, tactic {* clarsimp_tac @{clasimpset} 3 *},
   rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
   erule_tac [3] conseq12)
 apply         (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
@@ -365,7 +364,7 @@
   shows "finite U ==> uG = mgt_call`U ==>  
   !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. wt c --> P G {mgt c})"
 apply (induct_tac n)
-apply  (tactic {* ALLGOALS (CLASIMPSET' clarsimp_tac) *})
+apply  (tactic {* ALLGOALS (clarsimp_tac @{clasimpset}) *})
 apply  (subgoal_tac "G = mgt_call ` U")
 prefer 2
 apply   (simp add: card_seteq finite_imageI)