diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Datatypes.thy
--- a/Nominal/Ex/Datatypes.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Datatypes.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -53,7 +53,7 @@
 
 
 nominal_datatype baz =
-  Baz x::name t::foo bind x in t
+  Baz x::name t::foo   binds x in t
 
 
 
@@ -78,7 +78,7 @@
   Set_ty "nat set"
 | Fun "nat \<Rightarrow> nat"
 | Var "name"
-| Lam x::"name" t::"set_ty" bind x in t
+| Lam x::"name" t::"set_ty" binds x in t
 thm meta_eq_to_obj_eq
 thm set_ty.distinct
 thm set_ty.induct