--- a/src/HOL/Bali/AxSem.thy Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Bali/AxSem.thy Thu Sep 26 10:51:29 2002 +0200
@@ -413,7 +413,7 @@
"{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"
lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
-apply (rule injI)
+apply (rule inj_onI)
apply auto
done