# HG changeset patch
# User krauss
# Date 1286743825 -7200
# Node ID f225a499a8e50cc260ad48c9662dfd7b49b456d1
# Parent  8a2c7547835728ac3e2ff662c1e6762d88d60016
removed output syntax "'a ~=> 'b" for "'a => 'b option"

diff -r 8a2c75478357 -r f225a499a8e5 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Wed Oct 13 09:56:00 2010 +0200
+++ b/src/HOL/Map.thy	Sun Oct 10 22:50:25 2010 +0200
@@ -12,7 +12,6 @@
 begin
 
 types ('a,'b) "map" = "'a => 'b option" (infixr "~=>" 0)
-translations (type) "'a ~=> 'b" <= (type) "'a => 'b option"
 
 type_notation (xsymbols)
   "map" (infixr "\<rightharpoonup>" 0)