# HG changeset patch
# User haftmann
# Date 1196236899 -3600
# Node ID 65de74f62874c47ffcdb5d65cbe902715cedd6ca
# Parent  4ed49eccb1eb806a290c5933a4f8ee61266b2678
dropped legacy unnamed infix

diff -r 4ed49eccb1eb -r 65de74f62874 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Wed Nov 28 09:01:37 2007 +0100
+++ b/src/HOL/Map.thy	Wed Nov 28 09:01:39 2007 +0100
@@ -12,11 +12,11 @@
 imports List
 begin
 
-types ('a,'b) "~=>" = "'a => 'b option"  (infixr 0)
+types ('a,'b) map = "'a => 'b option"  (infixr "~=>" 0)
 translations (type) "a ~=> b " <= (type) "a => b option"
 
 syntax (xsymbols)
-  "~=>" :: "[type, type] => type"  (infixr "\<rightharpoonup>" 0)
+  map :: "type \<Rightarrow> type \<Rightarrow> type"  (infixr "\<rightharpoonup>" 0)
 
 abbreviation
   empty :: "'a ~=> 'b" where