src/HOL/Nominal/Examples/Fsub.thy

        with great help from Markus Wenzel. *}
 
 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 
   type-variables and to term-variables. These two kinds of names are represented in 
   the nominal datatype package as atom-types @{text "tyvrs"} and @{text "vrs"}: *}