# HG changeset patch
# User paulson
# Date 943352322 -3600
# Node ID 636884ec8f13d9f6efc12415b620210d0c67e9c5
# Parent  61dde9078e245dcdd9d6e98fb4731c6b43fba98d
tidied

diff -r 61dde9078e24 -r 636884ec8f13 src/HOL/equalities.ML
--- 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)";