--- a/Nominal/Ex/LF.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/LF.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -8,16 +8,16 @@
 nominal_datatype lf:
     kind =
       Type
-    | KPi "ty" n::"name" k::"kind" bind n in k
+    | KPi "ty" n::"name" k::"kind" binds n in k
 and ty =
       TConst "ident"
     | TApp "ty" "trm"
-    | TPi "ty" n::"name" ty::"ty"   bind n in ty
+    | TPi "ty" n::"name" ty::"ty"   binds n in ty
 and trm =
       Const "ident"
     | Var "name"
     | App "trm" "trm"
-    | Lam' "ty" n::"name" t::"trm"  bind n in t
+    | Lam' "ty" n::"name" t::"trm"  binds n in t
 
 abbreviation
   KPi_syn::"name \<Rightarrow> ty \<Rightarrow> kind \<Rightarrow> kind" ("\<Pi>[_:_]._" [100,100,100] 100)