diff -r 85fb70b0c5e8 -r 88bee9f6eec7 src/HOL/Proofs/Lambda/Commutation.thy
--- a/src/HOL/Proofs/Lambda/Commutation.thy	Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Proofs/Lambda/Commutation.thy	Fri May 13 22:55:00 2011 +0200
@@ -127,9 +127,9 @@
 
 lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
   apply (unfold square_def commute_def diamond_def Church_Rosser_def)
-  apply (tactic {* safe_tac HOL_cs *})
+  apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
    apply (tactic {*
-     blast_tac (HOL_cs addIs
+     blast_tac (put_claset HOL_cs @{context} addIs
        [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
         @{thm rtranclp_converseI}, @{thm conversepI},
         @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *})