diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/NoneExamples.thy
--- a/Nominal/Ex/NoneExamples.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/NoneExamples.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -20,8 +20,8 @@
   Foo_var "name"
 | Foo_pair "weird" "weird" 
 | Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
-    bind x in p1 p2, 
-    bind y in p2 p3
+    binds x in p1 p2, 
+    binds y in p2 p3
 *)
 
 text {* 
@@ -32,8 +32,8 @@
 (*
 nominal_datatype trm =
   Var "name"
-| Lam x::"name" t::"trm"         bind x in t
-| Let left::"trm" right::"trm"   bind (set) "bv left" in right
+| Lam x::"name" t::"trm"         binds x in t
+| Let left::"trm" right::"trm"   binds (set) "bv left" in right
 binder
   bv
 where
@@ -50,8 +50,8 @@
 (*
 nominal_datatype trm' =
   Var "name"
-| Lam l::"name" r::"trm'"   bind l in r
-| Let l::"trm'" r::"trm'"   bind (set) "bv' l" in r
+| Lam l::"name" r::"trm'"   binds l in r
+| Let l::"trm'" r::"trm'"   binds (set) "bv' l" in r
 binder
   bv'
 where
@@ -67,9 +67,9 @@
 (*
 nominal_datatype trm =
   Var "name"
-| Lam n::"name" l::"trm" bind n in l
+| Lam n::"name" l::"trm" binds n in l
 and bla =
-  Bla f::"trm" s::"trm" bind (set) "bv f" in s
+  Bla f::"trm" s::"trm" binds (set) "bv f" in s
 binder
   bv :: "trm \<Rightarrow> atom set"
 where
@@ -90,9 +90,9 @@
   Var "name"
 and bla =
   App "trm" "trm"
-| Bla1 f::"trm" s1::"trm" s2::"trm"  bind "bv f" in s1 f,  bind "bv f" in s2 f
-| Bla2 f::"trm" s1::"trm" s2::"trm"  bind "bv f" in s1,  bind "bv f" in s2 f
-| Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" bind "bv f" x in s1 f, bind y x in s2 
+| Bla1 f::"trm" s1::"trm" s2::"trm"  binds "bv f" in s1 f,  binds "bv f" in s2 f
+| Bla2 f::"trm" s1::"trm" s2::"trm"  binds "bv f" in s1,  binds "bv f" in s2 f
+| Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" binds "bv f" x in s1 f, binds y x in s2 
 binder
   bv :: "trm \<Rightarrow> atom list"
 where