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