src/HOL/Lambda/Commutation.ML

--- a/src/HOL/Lambda/Commutation.ML	Wed Apr 23 11:18:29 1997 +0200
+++ b/src/HOL/Lambda/Commutation.ML	Wed Apr 23 11:20:18 1997 +0200
@@ -94,6 +94,6 @@
        rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
 by (etac rtrancl_induct 1);
  by (Blast_tac 1);
-by (blast_tac (!claset delrules [rtrancl_refl] 
-                       addIs [r_into_rtrancl, rtrancl_trans]) 1);
+by (Blast.depth_tac (!claset delrules [rtrancl_refl] 
+                       addIs [r_into_rtrancl, rtrancl_trans]) 12 1);
 qed "Church_Rosser_confluent";