diff -r f1522b892a4c -r 5a176b8dda84 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Aug 29 16:15:11 2002 +0200
+++ b/src/HOL/Set.thy	Fri Aug 30 16:42:45 2002 +0200
@@ -343,22 +343,6 @@
   "'a set"}.
 *}
 
-ML {*
-  fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type);
-*}
-
-ML "
-  (* While (:) is not, its type must be kept
-    for overloading of = to work. *)
-  Blast.overloaded (\"op :\", domain_type);
-
-  overload_1st_set \"Ball\";            (*need UNION, INTER also?*)
-  overload_1st_set \"Bex\";
-
-  (*Image: retain the type of the set being expressed*)
-  Blast.overloaded (\"image\", domain_type);
-"
-
 lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
   -- {* Rule in Modus Ponens style. *}
   by (unfold subset_def) blast