diff -r 85fb70b0c5e8 -r 88bee9f6eec7 src/HOL/Hoare_Parallel/OG_Examples.thy
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Fri May 13 22:55:00 2011 +0200
@@ -170,10 +170,10 @@
 --{* 35 vc *}
 apply simp_all
 --{* 21 vc *}
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
 --{* 11 vc *}
 apply simp_all
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
 --{* 10 subgoals left *}
 apply(erule less_SucE)
  apply simp
@@ -430,13 +430,13 @@
  .{ \<forall>k<length a. (a ! k)=(\<acute>b ! k)}."
 apply oghoare
 --{* 138 vc  *}
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
 --{* 112 subgoals left *}
 apply(simp_all (no_asm))
 --{* 97 subgoals left *}
 apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
 --{* 930 subgoals left *}
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
 --{* 99 subgoals left *}
 apply(simp_all (*asm_lr*) only:length_0_conv [THEN sym])
 --{* 20 subgoals left *}
@@ -535,7 +535,7 @@
  .{\<acute>x=n}."
 apply oghoare
 apply (simp_all cong del: strong_setsum_cong)
-apply (tactic {* ALLGOALS (clarify_tac @{claset}) *})
+apply (tactic {* ALLGOALS (clarify_tac @{context}) *})
 apply (simp_all cong del: strong_setsum_cong)
    apply(erule (1) Example2_lemma2)
   apply(erule (1) Example2_lemma2)