--- a/Nominal/Ex/SystemFOmega.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/SystemFOmega.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -19,9 +19,9 @@
 nominal_datatype ty =
   TVar tvar
 | TFun ty ty
-| TAll a::tvar kind t::ty  bind a in t
-| TEx  a::tvar kind t::ty  bind a in t
-| TLam a::tvar kind t::ty  bind a in t
+| TAll a::tvar kind t::ty  binds a in t
+| TEx  a::tvar kind t::ty  binds a in t
+| TLam a::tvar kind t::ty  binds a in t
 | TApp ty ty
 | TRec trec
 and trec =
@@ -30,13 +30,13 @@
 
 nominal_datatype trm =
   Var var
-| Lam x::var ty t::trm  bind x in t
+| Lam x::var ty t::trm  binds x in t
 | App trm trm
 | Dot trm label
-| LAM a::tvar kind t::trm  bind a in t
+| LAM a::tvar kind t::trm  binds a in t
 | APP trm ty
 | Pack ty trm
-| Unpack a::tvar x::var trm t::trm  bind a x in t
+| Unpack a::tvar x::var trm t::trm  binds a x in t
 | Rec rec 
 and rec =
   RNil