1.1 --- a/src/HOL/Relation.ML	Wed Aug 19 10:26:37 1998 +0200
     1.2 +++ b/src/HOL/Relation.ML	Wed Aug 19 10:27:00 1998 +0200
     1.3 @@ -174,6 +174,8 @@
     1.4  
     1.5  (*** Image of a set under a relation ***)
     1.6  
     1.7 +Blast.overloaded ("Relation.op ^^", HOLogic.dest_setT o domain_type);
     1.8 +
     1.9  qed_goalw "Image_iff" thy [Image_def]
    1.10      "b : r^^A = (? x:A. (x,b):r)"
    1.11   (fn _ => [ Blast_tac 1 ]);