src/ZF/Perm.thy

--- a/src/ZF/Perm.thy	Wed Aug 21 15:57:08 2002 +0200
+++ b/src/ZF/Perm.thy	Wed Aug 21 15:57:24 2002 +0200
@@ -97,9 +97,10 @@
 apply (blast dest: Pair_mem_PiD)
 done
 
-lemma inj_apply_equality: "[| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b"
+lemma inj_apply_equality: "[| f:inj(A,B);  f`a=f`b;  a:A;  b:A |] ==> a=b"
 by (unfold inj_def, blast)
 
+
 (** A function with a left inverse is an injection **)
 
 lemma f_imp_injective: "[| f: A->B;  ALL x:A. d(f`x)=x |] ==> f: inj(A,B)"