src/HOL/Set.ML

 by (blast_tac (!claset addEs [equalityE]) 1);
 qed "singleton_inject";
 
 (*Redundant? But unlike insertCI, it proves the subgoal immediately!*)
 AddSIs [singletonI];   
-    
 AddSDs [singleton_inject];
+AddSEs [singletonE];
 
 goal Set.thy "{x.x=a} = {a}";
 by(Blast_tac 1);
 qed "singleton_conv";
 Addsimps [singleton_conv];