# HG changeset patch
# User paulson
# Date 903515245 -7200
# Node ID 721bf1a13f1a5ca4aa24a3ef6e9221d1bea60e9a
# Parent  07fb8999de623adf3468c88d70f391cc13b4ebf0
fixed overloading of "image"

diff -r 07fb8999de62 -r 721bf1a13f1a src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Aug 19 10:27:00 1998 +0200
+++ b/src/HOL/Set.ML	Wed Aug 19 10:27:25 1998 +0200
@@ -125,7 +125,7 @@
 (*need UNION, INTER also?*)
 
 (*Image: retain the type of the set being expressed*)
-Blast.overloaded ("op ``", domain_type o domain_type);
+Blast.overloaded ("op ``", domain_type);
 
 (*Rule in Modus Ponens style*)
 Goalw [subset_def] "[| A <= B;  c:A |] ==> c:B";