# HG changeset patch
# User paulson
# Date 861787218 -7200
# Node ID 005d899b5c484d0c15c5ff1795a011885ad6f821
# Parent  01364e2f30adbe3d08756afc98377bdbaf2d127f
Necessary inclusion of depth bound into blast_tac call

diff -r 01364e2f30ad -r 005d899b5c48 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";