1.1 --- a/src/HOL/Set.ML	Thu Nov 11 10:24:14 1999 +0100
     1.2 +++ b/src/HOL/Set.ML	Thu Nov 11 10:25:17 1999 +0100
     1.3 @@ -135,7 +135,7 @@
     1.4  overload_1st_set "Bex";
     1.5  
     1.6  (*Image: retain the type of the set being expressed*)
     1.7 -Blast.overloaded ("op ``", domain_type);
     1.8 +Blast.overloaded ("image", domain_type);
     1.9  
    1.10  (*Rule in Modus Ponens style*)
    1.11  Goalw [subset_def] "[| A <= B;  c:A |] ==> c:B";

     2.1 --- a/src/HOL/Set.thy	Thu Nov 11 10:24:14 1999 +0100
     2.2 +++ b/src/HOL/Set.thy	Thu Nov 11 10:25:17 1999 +0100
     2.3 @@ -35,7 +35,7 @@
     2.4    Pow           :: 'a set => 'a set set                 (*powerset*)
     2.5    range         :: ('a => 'b) => 'b set                 (*of function*)
     2.6    Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
     2.7 -  "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
     2.8 +  "image"       :: ['a => 'b, 'a set] => ('b set)   (infixr "``" 90)
     2.9    (*membership*)
    2.10    "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
    2.11  

     3.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Nov 11 10:24:14 1999 +0100
     3.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Nov 11 10:25:17 1999 +0100
     3.3 @@ -31,7 +31,7 @@
     3.4  
     3.5  (* figure out internal names *)
     3.6  
     3.7 -val image_name = Sign.intern_const (Theory.sign_of Set.thy) "op ``";
     3.8 +val image_name = Sign.intern_const (Theory.sign_of Set.thy) "image";
     3.9  val UNIV_name = Sign.intern_const (Theory.sign_of Set.thy) "UNIV";
    3.10  val inj_on_name = Sign.intern_const (Theory.sign_of Fun.thy) "inj_on";
    3.11  val inv_name = Sign.intern_const (Theory.sign_of Fun.thy) "inv";