--- a/src/HOL/Nominal/Examples/Fsub.thy Mon Aug 31 20:56:24 2015 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Mon Aug 31 21:01:21 2015 +0200
@@ -17,7 +17,7 @@
section {* Types for Names, Nominal Datatype Declaration for Types and Terms *}
no_syntax
- "_Map" :: "maplets => 'a ~=> 'b" ("(1[_])")
+ "_Map" :: "maplets => 'a \<rightharpoonup> 'b" ("(1[_])")
text {* The main point of this solution is to use names everywhere (be they bound,
binding or free). In System \FSUB{} there are two kinds of names corresponding to