src/HOL/Trancl.ML

--- a/src/HOL/Trancl.ML	Fri Sep 11 16:25:24 1998 +0200
+++ b/src/HOL/Trancl.ML	Fri Sep 11 16:25:40 1998 +0200
@@ -133,9 +133,8 @@
 qed "rtrancl_subset";
 
 Goal "(R^* Un S^*)^* = (R Un S)^*";
-(*Blast_tac: PROOF FAILED*)
-by (Blast.depth_tac (claset() addSIs [rtrancl_subset]
-                       addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 4 1);
+by (blast_tac (claset() addSIs [rtrancl_subset]
+                        addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
 qed "rtrancl_Un_rtrancl";
 
 Goal "(R^=)^* = R^*";