1.1 --- a/src/HOL/equalities.ML	Wed Nov 24 12:12:36 1999 +0100
     1.2 +++ b/src/HOL/equalities.ML	Wed Nov 24 13:35:31 1999 +0100
     1.3 @@ -472,7 +472,7 @@
     1.4  
     1.5  (*Basic identities*)
     1.6  
     1.7 -bind_thm ("not_empty", prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]));
     1.8 +bind_thm ("not_empty", prove_goal thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]));
     1.9  
    1.10  Goal "(UN x:{}. B x) = {}";
    1.11  by (Blast_tac 1);