# HG changeset patch
# User haftmann
# Date 1239883332 -7200
# Node ID db5dcc1f276d02b3d20038f96bcf03a12ba097a1
# Parent  ed5377c2b0a33fe13944b2289200e7d6cd0e19d6
dropped unnamed infix

diff -r ed5377c2b0a3 -r db5dcc1f276d src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu Apr 16 14:02:11 2009 +0200
+++ b/src/HOL/Map.thy	Thu Apr 16 14:02:12 2009 +0200
@@ -11,7 +11,7 @@
 imports List
 begin
 
-types ('a,'b) "~=>" = "'a => 'b option"  (infixr 0)
+types ('a,'b) "~=>" = "'a => 'b option"  (infixr "~=>" 0)
 translations (type) "a ~=> b " <= (type) "a => b option"
 
 syntax (xsymbols)