--- a/src/HOL/Relation.ML Thu Oct 15 11:35:07 1998 +0200
+++ b/src/HOL/Relation.ML Thu Oct 15 11:38:39 1998 +0200
@@ -174,7 +174,7 @@
(*** Image of a set under a relation ***)
-Blast.overloaded ("Relation.op ^^", HOLogic.dest_setT o domain_type);
+overload_1st_set "Relation.op ^^";
qed_goalw "Image_iff" thy [Image_def]
"b : r^^A = (? x:A. (x,b):r)"
--- a/src/HOL/Set.ML Thu Oct 15 11:35:07 1998 +0200
+++ b/src/HOL/Set.ML Thu Oct 15 11:38:39 1998 +0200
@@ -117,12 +117,16 @@
by (REPEAT (ares_tac (prems @ [ballI]) 1));
qed "subsetI";
+(*Map the type ('a set => anything) to just 'a.
+ For overloading constants whose first argument has type "'a set" *)
+fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type);
+
(*While (:) is not, its type must be kept
for overloading of = to work.*)
Blast.overloaded ("op :", domain_type);
-seq (fn a => Blast.overloaded (a, HOLogic.dest_setT o domain_type))
- ["Ball", "Bex"];
-(*need UNION, INTER also?*)
+
+overload_1st_set "Ball"; (*need UNION, INTER also?*)
+overload_1st_set "Bex";
(*Image: retain the type of the set being expressed*)
Blast.overloaded ("op ``", domain_type);