
diff -r 6cb92c2a5ece -r aefe89038dd2 src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Mon Aug 31 20:56:24 2015 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Mon Aug 31 21:01:21 2015 +0200
@@ -5,7 +5,7 @@
 begin
 
 no_syntax
-  "_Map" :: "maplets => 'a ~=> 'b"  ("(1[_])")
+  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  ("(1[_])")
 
 atom_decl name
 




