
diff -r be1d3b8cfbd5 -r b807858b97bd src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Mon Aug 02 10:12:02 2004 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Mon Aug 02 10:15:37 2004 +0200
@@ -316,7 +316,6 @@
 apply(  assumption)
 apply( fast)
 apply(auto dest!: wf_cdecl_supD)
-(*CBtrancl: apply(erule (1) converse_rtrancl_into_rtrancl) *)
 done
 
 lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"




