diff -r 3736cf381e15 -r db4005b40cc6 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Sep 26 10:51:29 2002 +0200
@@ -230,7 +230,7 @@
 apply(  simp add: wf_cdecl_def)
 apply(  rule unique_map_inj)
 apply(   simp)
-apply(  rule injI)
+apply(  rule inj_onI)
 apply(  simp)
 apply( safe dest!: wf_cdecl_supD)
 apply( drule subcls1_wfD)
@@ -244,7 +244,7 @@
 apply( erule unique_append)
 apply(  rule unique_map_inj)
 apply(   clarsimp)
-apply  (rule injI)
+apply  (rule inj_onI)
 apply(  simp)
 apply(auto dest!: widen_fields_defpl)
 done