Tidied proof of r_comp_rtrancl_eq

--- a/src/HOL/Trancl.ML	Mon Sep 29 11:32:25 1997 +0200
+++ b/src/HOL/Trancl.ML	Mon Sep 29 11:36:44 1997 +0200
@@ -195,9 +195,8 @@
 qed "rtranclE2";
 
 goal Trancl.thy "r O r^* = r^* O r";
-by (Step_tac 1);
- by (blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1);
-by (blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1);
+by (blast_tac (!claset addEs [rtranclE, rtranclE2] 
+	               addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
 qed "r_comp_rtrancl_eq";