src/HOL/Fun.ML

--- a/src/HOL/Fun.ML	Mon Mar 11 14:03:30 1996 +0100
+++ b/src/HOL/Fun.ML	Mon Mar 11 14:04:37 1996 +0100
@@ -177,6 +177,7 @@
             ComplI, IntI, DiffI, UnCI, insertCI] 
     addIs  [bexI, UnionI, UN_I, UN1_I, imageI, rangeI] 
     addSEs [bexE, make_elim PowD, UnionE, UN_E, UN1_E, DiffE,
+	    make_elim singleton_inject,
             CollectE, ComplE, IntE, UnE, insertE, imageE, rangeE, emptyE] 
     addEs  [ballE, InterD, InterE, INT_D, INT_E, make_elim INT1_D,
             subsetD, subsetCE];