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