diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/Transitive_Closure_lemmas.ML
--- a/src/HOL/Transitive_Closure_lemmas.ML	Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/Transitive_Closure_lemmas.ML	Thu Dec 20 18:22:44 2001 +0100
@@ -68,7 +68,7 @@
 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
 qed "rtranclE";
 
-bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
+bind_thm ("converse_rtrancl_into_rtrancl", r_into_rtrancl RS rtrancl_trans);
 
 (*** More r^* equations and inclusions ***)
 
@@ -167,7 +167,7 @@
 
 Goal "r O r^* = r^* O r";
 by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] 
-	               addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
+	               addIs [rtrancl_into_rtrancl, converse_rtrancl_into_rtrancl]) 1);
 qed "r_comp_rtrancl_eq";