diff -r d33a5d59a29a -r e60a230da179 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Sep 09 10:59:32 1996 +0200
+++ b/src/HOL/Set.thy	Mon Sep 09 11:08:01 1996 +0200
@@ -31,7 +31,7 @@
   Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
   inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
   inj_onto      :: ['a => 'b, 'a set] => bool
-  "``"          :: ['a => 'b, 'a set] => ('b set)   (infixl 90)
+  "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
   ":"           :: ['a, 'a set] => bool             (infixl 50) (*membership*)