--- 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