src/HOL/UNITY/WFair.thy

--- a/src/HOL/UNITY/WFair.thy	Wed Feb 24 22:04:10 2010 +0100
+++ b/src/HOL/UNITY/WFair.thy	Wed Feb 24 22:09:50 2010 +0100
@@ -69,8 +69,8 @@
      --{*predicate transformer: the largest set that leads to @{term B}*}
     "wlt F B == Union {A. F \<in> A leadsTo B}"
 
-syntax (xsymbols)
-  "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
+notation (xsymbols)
+  leadsTo  (infixl "\<longmapsto>" 60)
 
 
 subsection{*transient*}