diff -r 024bdf8e52a4 -r e33b47e4246d src/HOL/Inverse_Image.thy
--- a/src/HOL/Inverse_Image.thy	Tue Jan 09 15:18:07 2001 +0100
+++ b/src/HOL/Inverse_Image.thy	Tue Jan 09 15:22:13 2001 +0100
@@ -9,7 +9,7 @@
 Inverse_Image = Set +
 
 constdefs
-  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-``" 90)
-    "f-``B  == {x. f(x) : B}"
+  vimage :: ['a => 'b, 'b set] => ('a set)   (infixr "-`" 90)
+    "f-`B  == {x. f(x) : B}"
 
 end