prove_goal thy;

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