# HG changeset patch
# User paulson
# Date 908444319 -7200
# Node ID 1bac26652f4571b8df3a8bfe89b9f485f64bc411
# Parent  fe887910e32ebd122ac53e71c2b0695e9adf2b8f
Uses overload_1st_set to specify overloading

diff -r fe887910e32e -r 1bac26652f45 src/HOL/Relation.ML
--- 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)"
diff -r fe887910e32e -r 1bac26652f45 src/HOL/Set.ML
--- 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);