diff -r 649c46adfccc -r 33d23d0a300e src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Jan 28 14:07:33 2000 +0100
+++ b/src/HOL/Fun.ML	Fri Jan 28 14:07:53 2000 +0100
@@ -169,6 +169,11 @@
 by (Blast_tac 1);
 qed "inj_on_contraD";
 
+Goal "inj (%s. {s})";
+br injI 1;
+be singleton_inject 1;
+qed "inj_singleton";
+
 Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
 by (Blast_tac 1);
 qed "subset_inj_on";