--- a/src/HOL/Lambda/Commutation.ML	Fri May 26 18:04:17 2000 +0200
+++ b/src/HOL/Lambda/Commutation.ML	Fri May 26 18:05:34 2000 +0200
@@ -78,8 +78,8 @@
 qed "confluent_Un";
 
 Goal "[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
-by (fast_tac (claset() addIs [diamond_confluent] addDs [rtrancl_subset RS sym] 
-		       addss simpset()) 1);
+by (force_tac (claset() addIs [diamond_confluent] 
+                        addDs [rtrancl_subset RS sym], simpset()) 1);
 qed "diamond_to_confluence";
 
 (*** Church_Rosser ***)