new-style infix declaration for "image"

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

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

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