--- 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 *})