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";