diff -r e28553315355 -r d78cf498a88c src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/Set.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -412,8 +412,8 @@
 
 (*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);