# HG changeset patch
# User oheimb
# Date 982691249 -3600
# Node ID eca861fd1eb5c00691a542106e108fa92546779c
# Parent  3b69feb7d0531a41a1e779a14300cd9f53180590
simplified definition of wrapper bspec

diff -r 3b69feb7d053 -r eca861fd1eb5 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Feb 20 18:47:27 2001 +0100
+++ b/src/HOL/Set.ML	Tue Feb 20 18:47:29 2001 +0100
@@ -61,8 +61,7 @@
 AddEs  [ballE];
 AddXDs [bspec];
 (* gives better instantiation for bound: *)
-claset_ref() := claset() addWrapper ("bspec", fn tac2 =>
-			 (dtac bspec THEN' atac) APPEND' tac2);
+claset_ref() := claset() addbefore ("bspec", datac bspec 1);
 
 (*Normally the best argument order: P(x) constrains the choice of x:A*)
 Goalw [Bex_def] "[| P(x);  x:A |] ==> EX x:A. P(x)";