tidied

--- a/src/HOL/equalities.ML	Tue Nov 23 11:18:19 1999 +0100
+++ b/src/HOL/equalities.ML	Tue Nov 23 11:18:42 1999 +0100
@@ -782,7 +782,7 @@
 qed "ex_bool_eq";
 
 Goal "A Un B = (UN b. if b then A else B)";
-by (auto_tac(claset()delWrapper"bspec",simpset()addsimps [split_if_mem2]));
+by (auto_tac(claset(), simpset() addsimps [split_if_mem2]));
 qed "Un_eq_UN";
 
 Goal "(UN b::bool. A b) = (A True Un A False)";