fixed overloading of "image"
authorpaulson
Wed Aug 19 10:27:25 1998 +0200 (1998-08-19)
changeset 5336721bf1a13f1a
parent 5335 07fb8999de62
child 5337 2f7d09a927c4
fixed overloading of "image"
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Wed Aug 19 10:27:00 1998 +0200
     1.2 +++ b/src/HOL/Set.ML	Wed Aug 19 10:27:25 1998 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4  (*need UNION, INTER also?*)
     1.5  
     1.6  (*Image: retain the type of the set being expressed*)
     1.7 -Blast.overloaded ("op ``", domain_type o domain_type);
     1.8 +Blast.overloaded ("op ``", domain_type);
     1.9  
    1.10  (*Rule in Modus Ponens style*)
    1.11  Goalw [subset_def] "[| A <= B;  c:A |] ==> c:B";