diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Set.thy	Tue Jan 09 15:22:13 2001 +0100
@@ -34,7 +34,7 @@
   Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
   Pow           :: 'a set => 'a set set                 (*powerset*)
   Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
-  "image"       :: ['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)
 
@@ -70,7 +70,7 @@
   "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
 
 translations
-  "range f"     == "f``UNIV"
+  "range f"     == "f`UNIV"
   "x ~: y"      == "~ (x : y)"
   "{x, xs}"     == "insert x {xs}"
   "{x}"         == "insert x {}"
@@ -145,7 +145,7 @@
   empty_def     "{}             == {x. False}"
   UNIV_def      "UNIV           == {x. True}"
   insert_def    "insert a B     == {x. x=a} Un B"
-  image_def     "f``A           == {y. ? x:A. y=f(x)}"
+  image_def     "f`A           == {y. ? x:A. y=f(x)}"
 
 
 end