src/HOL/Fun.ML

--- a/src/HOL/Fun.ML	Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/Fun.ML	Thu Sep 26 12:47:47 1996 +0200
@@ -173,7 +173,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,
+            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];