diff -r 9df4b3934487 -r fe20540bcf93 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Thu Dec 20 17:08:55 2001 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Dec 20 18:22:44 2001 +0100
@@ -178,7 +178,7 @@
 apply(  assumption)
 apply( fast)
 apply(auto dest!: wf_cdecl_supD)
-apply(erule (1) rtrancl_into_rtrancl2)
+apply(erule (1) converse_rtrancl_into_rtrancl)
 done
 
 lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"