# HG changeset patch
# User haftmann
# Date 1196259999 -3600
# Node ID e8ab1c42c14f043974c5e591c6e3ed3a2a345d86
# Parent  5b0625f6e324fd52055c98e69153930c4b6fa05c
(reverted to unnamed infix)

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