AddXDs [bspec];

--- a/src/ZF/ZF.ML	Thu Sep 09 12:25:44 1999 +0200
+++ b/src/ZF/ZF.ML	Thu Sep 09 12:26:45 1999 +0200
@@ -46,6 +46,7 @@
 
 AddSIs [ballI];
 AddEs  [rev_ballE];
+AddXDs [bspec];
 
 (*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
 val ball_tac = dtac bspec THEN' assume_tac;