diff -r a6cd1a454751 -r 4b3d280ef06a src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Thu Jul 22 19:33:12 2004 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Mon Jul 26 15:48:50 2004 +0200
@@ -316,7 +316,7 @@
 apply(  assumption)
 apply( fast)
 apply(auto dest!: wf_cdecl_supD)
-apply(erule (1) converse_rtrancl_into_rtrancl)
+(*CBtrancl: apply(erule (1) converse_rtrancl_into_rtrancl) *)
 done
 
 lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"