--- a/Nominal/Ex/Classical.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Classical.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -10,27 +10,27 @@
 
 nominal_datatype trm =
   Ax "name" "coname"
-| Cut c::"coname" t1::"trm" n::"name" t2::"trm"             bind n in t1, bind c in t2  
+| Cut c::"coname" t1::"trm" n::"name" t2::"trm"             binds n in t1, binds c in t2  
      ("Cut <_>._ '(_')._" [100,100,100,100] 100)
-| NotR n::"name" t::"trm" "coname"                            bind n in t
+| NotR n::"name" t::"trm" "coname"                            binds n in t
      ("NotR '(_')._ _" [100,100,100] 100)
-| NotL c::"coname" t::"trm" "name"                            bind c in t   
+| NotL c::"coname" t::"trm" "name"                            binds c in t   
      ("NotL <_>._ _" [100,100,100] 100)
-| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2
+| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" binds c1 in t1, binds c2 in t2
      ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100)
-| AndL1 n::"name" t::"trm" "name"                             bind n in t
+| AndL1 n::"name" t::"trm" "name"                             binds n in t
      ("AndL1 '(_')._ _" [100,100,100] 100)
-| AndL2 n::"name" t::"trm" "name"                             bind n in t
+| AndL2 n::"name" t::"trm" "name"                             binds n in t
      ("AndL2 '(_')._ _" [100,100,100] 100)
-| OrR1 c::"coname" t::"trm" "coname"                          bind c in t             
+| OrR1 c::"coname" t::"trm" "coname"                          binds c in t             
      ("OrR1 <_>._ _" [100,100,100] 100)
-| OrR2 c::"coname" t::"trm" "coname"                          bind c in t     
+| OrR2 c::"coname" t::"trm" "coname"                          binds c in t     
      ("OrR2 <_>._ _" [100,100,100] 100)
-| OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name"        bind n1 in t1, bind n2 in t2       
+| OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name"        binds n1 in t1, binds n2 in t2       
      ("OrL '(_')._ '(_')._ _" [100,100,100,100,100] 100)
-| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       bind c in t1, bind n in t2
+| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       binds c in t1, binds n in t2
      ("ImpL <_>._ '(_')._ _" [100,100,100,100,100] 100)
-| ImpR n::"name" c::"coname" t::"trm" "coname"                bind n c in t
+| ImpR n::"name" c::"coname" t::"trm" "coname"                binds n c in t
      ("ImpR '(_').<_>._ _" [100,100,100,100] 100)
 
 thm trm.distinct

--- a/Nominal/Ex/CoreHaskell.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/CoreHaskell.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -19,7 +19,7 @@
 | TC "string"
 | TApp "ty" "ty"
 | TFun "string" "ty_lst"
-| TAll tv::"tvar" "tkind" T::"ty"  bind (set) tv in T
+| TAll tv::"tvar" "tkind" T::"ty"  binds (set) tv in T
 | TEq "ckind" "ty"
 and ty_lst =
   TsNil
@@ -29,7 +29,7 @@
 | CConst "string"
 | CApp "co" "co"
 | CFun "string" "co_lst"
-| CAll cv::"cvar" "ckind" C::"co"  bind (set) cv in C
+| CAll cv::"cvar" "ckind" C::"co"  binds (set) cv in C
 | CEq "ckind" "co"
 | CRefl "ty"
 | CSym "co"
@@ -47,18 +47,18 @@
 and trm =
   Var "var"
 | K "string"
-| LAMT tv::"tvar" "tkind" t::"trm" bind (set) tv in t
-| LAMC cv::"cvar" "ckind" t::"trm" bind (set) cv in t
+| LAMT tv::"tvar" "tkind" t::"trm" binds (set) tv in t
+| LAMC cv::"cvar" "ckind" t::"trm" binds (set) cv in t
 | AppT "trm" "ty"
 | AppC "trm" "co"
-| Lam v::"var" "ty" t::"trm"       bind (set) v in t
+| Lam v::"var" "ty" t::"trm"       binds (set) v in t
 | App "trm" "trm"
-| Let x::"var" "ty" "trm" t::"trm" bind (set) x in t
+| Let x::"var" "ty" "trm" t::"trm" binds (set) x in t
 | Case "trm" "assoc_lst"
 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
 and assoc_lst =
   ANil
-| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t
+| ACons p::"pat" t::"trm" "assoc_lst" binds "bv p" in t
 and pat =
   Kpat "string" "tvars" "cvars" "vars"
 and vars =

--- a/Nominal/Ex/CoreHaskell2.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/CoreHaskell2.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -20,7 +20,7 @@
        Tvar tvar
      | Tcon string
      | Tapp Ty Ty
-     | Tforall pb::PBind ty::Ty   bind "bind_pb pb" in ty
+     | Tforall pb::PBind ty::Ty   binds "bind_pb pb" in ty
 and PBind =
   Pbind tvar Kind
 binder
@@ -37,7 +37,7 @@
      | Dcon string
      | App Exp Exp
      | Appt Exp Ty
-     | Lam b::Bind e::Exp bind "bind_b b" in e
+     | Lam b::Bind e::Exp binds "bind_b b" in e
 binder
   bind_b
 where

--- 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

--- a/Nominal/Ex/Ex1.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Ex1.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -10,10 +10,10 @@
 
 nominal_datatype foo =
   Foo0 "name"
-| Foo1 b::"bar" f::"foo" bind (set) "bv b" in f
+| Foo1 b::"bar" f::"foo" binds (set) "bv b" in f
 and bar =
   Bar0 "name"
-| Bar1 "name" s::"name" b::"bar" bind (set) s in b
+| Bar1 "name" s::"name" b::"bar" binds (set) s in b
 binder
   bv
 where

--- a/Nominal/Ex/ExPS3.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/ExPS3.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -9,8 +9,8 @@
 nominal_datatype exp =
   Var "name"
 | App "exp" "exp"
-| Lam x::"name" e::"exp" bind x in e
-| Let x::"name" p::"pat" e1::"exp" e2::"exp" bind (set) x in e2, bind (set) "bp p" in e1
+| Lam x::"name" e::"exp" binds x in e
+| Let x::"name" p::"pat" e1::"exp" e2::"exp" binds (set) x in e2, binds (set) "bp p" in e1
 and pat =
   PVar "name"
 | PUnit

--- a/Nominal/Ex/Foo1.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Foo1.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -13,11 +13,11 @@
 nominal_datatype foo: trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind x in t
-| Let1 a::"assg" t::"trm"  bind "bn1 a" in t
-| Let2 a::"assg" t::"trm"  bind "bn2 a" in t
-| Let3 a::"assg" t::"trm"  bind "bn3 a" in t
-| Let4 a::"assg'" t::"trm"  bind (set) "bn4 a" in t
+| Lam x::"name" t::"trm"    binds x in t
+| Let1 a::"assg" t::"trm"   binds "bn1 a" in t
+| Let2 a::"assg" t::"trm"   binds "bn2 a" in t
+| Let3 a::"assg" t::"trm"   binds "bn3 a" in t
+| Let4 a::"assg'" t::"trm"  binds (set) "bn4 a" in t
 and assg =
   As "name" "name" "trm"
 and assg' =

--- a/Nominal/Ex/Foo2.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Foo2.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -13,9 +13,9 @@
 nominal_datatype foo: trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind x in t
-| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" bind "bn a1" in t1, bind "bn a2" in t2
-| Let2 x::"name" y::"name" t1::"trm" t2::"trm" bind x y in t1, bind y in t2
+| Lam x::"name" t::"trm"  binds x in t
+| Let1 a1::"assg" t1::"trm" a2::"assg" t2::"trm" binds "bn a1" in t1, binds "bn a2" in t2
+| Let2 x::"name" y::"name" t1::"trm" t2::"trm" binds x y in t1, binds y in t2
 and assg =
   As_Nil
 | As "name" x::"name" t::"trm" "assg" 

--- 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)

--- a/Nominal/Ex/LamFun.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/LamFun.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -7,7 +7,7 @@
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
-| Lam x::"name" l::"lam"  bind x in l
+| Lam x::"name" l::"lam"  binds x in l
 
 thm lam.distinct
 thm lam.induct

--- a/Nominal/Ex/Lambda.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -1,5 +1,7 @@
 theory Lambda
-imports "../Nominal2" 
+imports 
+  "../Nominal2"
+  "~~/src/HOL/Library/Monad_Syntax"
 begin
 
 
@@ -8,7 +10,7 @@
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
-| Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
+| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
 ML {* Method.SIMPLE_METHOD' *}
 ML {* Sign.intern_const *}
@@ -320,24 +322,56 @@
 termination
   by lexicographic_order
 
+
+text {* count the occurences of lambdas in a term *}
+
+nominal_primrec
+  cntlams :: "lam  \<Rightarrow> nat"
+where
+  "cntlams (Var x) = 0"
+| "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)"
+| "cntlams (Lam [x]. t) = Suc (cntlams t)"
+  apply(simp add: eqvt_def cntlams_graph_def)
+  apply(rule, perm_simp, rule)
+  apply(rule TrueI)
+  apply(rule_tac y="x" in lam.exhaust)
+  apply(auto)[3]
+  apply(all_trivials)
+  apply(simp)
+  apply(simp)
+  apply(erule_tac c="()" in Abs_lst1_fcb2')
+  apply(simp add: pure_fresh)
+  apply(simp add: fresh_star_def pure_fresh)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  done
+
+termination
+  by lexicographic_order
+
+
 text {* count the bound-variable occurences in a lambda-term *}
 
 nominal_primrec
-  cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
+  cntbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
 where
-  "cbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
-| "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)"
-| "atom x \<sharp> xs \<Longrightarrow> cbvs (Lam [x]. t) xs = cbvs t (x # xs)"
-  apply(simp add: eqvt_def cbvs_graph_def)
+  "cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
+| "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)"
+| "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)"
+  apply(simp add: eqvt_def cntbvs_graph_def)
   apply(rule, perm_simp, rule)
-  apply(simp_all)
+  apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply(auto simp add: fresh_star_def)[3]
+  apply(all_trivials)
+  apply(simp)
+  apply(simp)
+  apply(simp)
   apply(erule conjE)
   apply(erule Abs_lst1_fcb2')
   apply(simp add: pure_fresh fresh_star_def)
-  apply(simp add: pure_fresh fresh_star_def)
+  apply(simp add: fresh_star_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
@@ -380,11 +414,14 @@
   "(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)"
   by (induct l arbitrary: n) (simp_all add: permute_pure)
 
+
+
 nominal_primrec
   transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option"
 where
   "transdb (Var x) l = vindex l x 0"
-| "transdb (App t1 t2) xs = Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
+| "transdb (App t1 t2) xs = 
+      Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
 | "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
   unfolding eqvt_def transdb_graph_def
   apply (rule, perm_simp, rule)
@@ -421,47 +458,6 @@
   Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
   using a by simp
 
-
-abbreviation
-  mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65) 
-where  
-  "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v"
-
-lemma mbind_eqvt:
-  fixes c::"'a::pt option"
-  shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"
-apply(cases c)
-apply(simp_all)
-apply(perm_simp)
-apply(rule refl)
-done
-
-lemma mbind_eqvt_raw[eqvt_raw]:
-  shows "(p \<bullet> option_case) \<equiv> option_case"
-apply(rule eq_reflection)
-apply(rule ext)+
-apply(case_tac xb)
-apply(simp_all)
-apply(rule_tac p="-p" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel)
-apply(simp)
-apply(rule_tac p="-p" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel)
-apply(simp)
-done
-
-fun
-  index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option" 
-where
-  "index [] n x = None"
-| "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))"
-
-lemma [eqvt]:
-  shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
-apply(induct xs arbitrary: n)
-apply(simp_all add: permute_pure)
-done
-
 lemma supp_subst:
   "supp (t[x ::= s]) \<subseteq> supp t \<union> supp s"
   by (induct t x s rule: subst.induct) (auto simp add: lam.supp)
@@ -569,13 +565,59 @@
 termination
   by lexicographic_order
 
+
+(*
+abbreviation
+  mbind :: "'a option => ('a => 'b option) => 'b option"  ("_ \<guillemotright>= _" [65,65] 65) 
+where  
+  "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v"
+
+lemma mbind_eqvt:
+  fixes c::"'a::pt option"
+  shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"
+apply(cases c)
+apply(simp_all)
+apply(perm_simp)
+apply(rule refl)
+done
+
+lemma mbind_eqvt_raw[eqvt_raw]:
+  shows "(p \<bullet> option_case) \<equiv> option_case"
+apply(rule eq_reflection)
+apply(rule ext)+
+apply(case_tac xb)
+apply(simp_all)
+apply(rule_tac p="-p" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel)
+apply(simp)
+apply(rule_tac p="-p" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel)
+apply(simp)
+done
+
+fun
+  index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option" 
+where
+  "index [] n x = None"
+| "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))"
+
+lemma [eqvt]:
+  shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
+apply(induct xs arbitrary: n)
+apply(simp_all add: permute_pure)
+done
+*)
+
+(*
 nominal_primrec
   trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
 where
-  "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"
-| "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
-| "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
+  "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n::nat. Some (DBVar n)))"
+| "trans2 (App t1 t2) xs = 
+     ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1::db. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2::db. Some (DBApp db1 db2))))"
+| "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db::db. Some (DBLam db)))"
 oops
+*)
 
 nominal_primrec
   CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"

--- a/Nominal/Ex/Lambda_F_T.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Lambda_F_T.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -7,7 +7,7 @@
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
-| Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
+| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
 lemma fresh_fun_eqvt_app3:
   assumes a: "eqvt f"

--- a/Nominal/Ex/Let.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Let.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -7,8 +7,8 @@
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind  x in t
-| Let as::"assn" t::"trm"   bind "bn as" in t
+| Lam x::"name" t::"trm"  binds  x in t
+| Let as::"assn" t::"trm"   binds "bn as" in t
 and assn =
   ANil
 | ACons "name" "trm" "assn"

--- a/Nominal/Ex/LetFun.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/LetFun.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -12,7 +12,7 @@
 nominal_datatype exp =
   Var name
 | Pair exp exp
-| LetRec x::name p::pat e1::exp e2::exp  bind x in e2, bind x "bp p" in e1
+| LetRec x::name p::pat e1::exp e2::exp  binds x in e2, binds x "bp p" in e1
 and pat =
   PVar name
 | PUnit

--- a/Nominal/Ex/LetInv.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/LetInv.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -7,8 +7,8 @@
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind  x in t
-| Let as::"assn" t::"trm"   bind "bn as" in t
+| Lam x::"name" t::"trm"    binds  x in t
+| Let as::"assn" t::"trm"   binds "bn as" in t
 and assn =
   ANil
 | ACons "name" "trm" "assn"

--- a/Nominal/Ex/LetPat.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/LetPat.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -7,8 +7,8 @@
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"       bind (set) x in t
-| Let p::"pat" "trm" t::"trm"  bind (set) "f p" in t
+| Lam x::"name" t::"trm"       binds (set) x in t
+| Let p::"pat" "trm" t::"trm"  binds (set) "f p" in t
 and pat =
   PN
 | PS "name"

--- a/Nominal/Ex/LetRec.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/LetRec.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -8,8 +8,8 @@
  trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"     bind (set) x in t
-| Let_Rec bp::"bp" t::"trm"  bind (set) "bn bp" in bp t
+| Lam x::"name" t::"trm"     binds (set) x in t
+| Let_Rec bp::"bp" t::"trm"  binds (set) "bn bp" in bp t
 and bp =
   Bp "name" "trm"
 binder

--- a/Nominal/Ex/LetRec2.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/LetRec2.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -7,8 +7,8 @@
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
-| Lm x::"name" t::"trm"  bind (set) x in t
-| Lt a::"lts" t::"trm"   bind "bn a" in a t
+| Lm x::"name" t::"trm"  binds (set) x in t
+| Lt a::"lts" t::"trm"   binds "bn a" in a t
 and lts =
   Lnil
 | Lcons "name" "trm" "lts"

--- a/Nominal/Ex/LetRecB.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/LetRecB.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -8,8 +8,8 @@
  trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"     bind x in t
-| Let_Rec bp::"bp" t::"trm"  bind "bn bp" in bp t
+| Lam x::"name" t::"trm"     binds x in t
+| Let_Rec bp::"bp" t::"trm"  binds "bn bp" in bp t
 and bp =
   Bp "name" "trm"
 binder

--- a/Nominal/Ex/LetSimple1.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/LetSimple1.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -7,7 +7,7 @@
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Let x::"name" "trm" t::"trm"   bind x in t
+| Let x::"name" "trm" t::"trm"   binds x in t
 
 print_theorems
 

--- a/Nominal/Ex/LetSimple2.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/LetSimple2.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -7,7 +7,7 @@
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Let as::"assn" t::"trm"   bind "bn as" in t
+| Let as::"assn" t::"trm"   binds "bn as" in t
 and assn =
   Assn "name" "trm"
 binder

--- a/Nominal/Ex/Let_ExhaustIssue.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Let_ExhaustIssue.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -8,8 +8,8 @@
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind  x in t
-| Let as::"assn" t::"trm"   bind "bn as" in t
+| Lam x::"name" t::"trm"  binds  x in t
+| Let as::"assn" t::"trm"   binds "bn as" in t
 and assn =
   ANil
 | ACons "name" "trm" "assn"

--- a/Nominal/Ex/Modules.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Modules.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -14,12 +14,12 @@
  mexp =
   Acc "path"
 | Stru "body"
-| Funct x::"name" "sexp" m::"mexp"    bind (set) x in m
+| Funct x::"name" "sexp" m::"mexp"    binds (set) x in m
 | FApp "mexp" "path"
 | Ascr "mexp" "sexp"
 and body =
   Empty
-| Seq c::"defn" d::"body"     bind (set) "cbinders c" in d
+| Seq c::"defn" d::"body"     binds (set) "cbinders c" in d
 and defn =
   Type "name" "ty"
 | Dty "name"
@@ -30,7 +30,7 @@
 | SFunc "name" "sexp" "sexp"
 and sbody =
   SEmpty
-| SSeq C::"spec" D::"sbody"    bind (set) "Cbinders C" in D
+| SSeq C::"spec" D::"sbody"    binds (set) "Cbinders C" in D
 and spec =
   Type1 "name"
 | Type2 "name" "ty"
@@ -46,7 +46,7 @@
 and trm =
   Tref1 "name"
 | Tref2 "path" "name"
-| Lam' v::"name" "ty" M::"trm"  bind (set) v in M
+| Lam' v::"name" "ty" M::"trm"  binds (set) v in M
 | App' "trm" "trm"
 | Let' "body" "trm"
 binder

--- a/Nominal/Ex/Multi_Recs.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Multi_Recs.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -15,7 +15,7 @@
   Var name
 | Unit
 | Pair exp exp
-| LetRec l::"lrbs" e::"exp"  bind (set) "bs l" in l e
+| LetRec l::"lrbs" e::"exp"  binds (set) "bs l" in l e
 and lrb =
   Assign name exp
 and lrbs =

--- a/Nominal/Ex/Multi_Recs2.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Multi_Recs2.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -17,9 +17,9 @@
   Var name
 | Unit 
 | Pair exp exp
-| LetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e
+| LetRec l::lrbs e::exp binds (set) "b_lrbs l" in l e
 and fnclause =
-  K x::name p::pat f::exp bind (set) "b_pat p" in f
+  K x::name p::pat f::exp binds (set) "b_pat p" in f
 and fnclauses =
   S fnclause
 | ORs fnclause fnclauses

--- 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

--- a/Nominal/Ex/Shallow.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Shallow.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -13,7 +13,7 @@
 nominal_datatype trm1 =
   Var1 "name"
 | App1 "trm1" "trm1"
-| Lam1 xs::"name list" t::"trm1" bind xs in t
+| Lam1 xs::"name list" t::"trm1" binds xs in t
 
 thm trm1.strong_exhaust
 
@@ -23,7 +23,7 @@
 nominal_datatype trm2 =
   Var2 "name"
 | App2 "trm2" "trm2"
-| Lam2 xs::"name fset" t::"trm2" bind (set) xs in t
+| Lam2 xs::"name fset" t::"trm2" binds (set) xs in t
 
 thm trm2.strong_exhaust
 
@@ -32,7 +32,7 @@
 nominal_datatype trm3 =
   Var3 "name"
 | App3 "trm3" "trm3"
-| Lam3 xs::"name fset" t::"trm3" bind (set+) xs in t
+| Lam3 xs::"name fset" t::"trm3" binds (set+) xs in t
 
 thm trm3.eq_iff
 

--- a/Nominal/Ex/SingleLet.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -7,13 +7,13 @@
 nominal_datatype single_let: trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind x in t
-| Let a::"assg" t::"trm"  bind "bn a" in t
-| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
-| Bar x::"name" y::"name" t::"trm" bind y x in t x y
-| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set+) x in t2 
+| Lam x::"name" t::"trm"  binds x in t
+| Let a::"assg" t::"trm"  binds "bn a" in t
+| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" binds (set) x in y t t1 t2
+| Bar x::"name" y::"name" t::"trm" binds y x in t x y
+| Baz x::"name" t1::"trm" t2::"trm" binds (set) x in t1, binds (set+) x in t2 
 and assg =
-  As "name" x::"name" t::"trm" bind x in t
+  As "name" x::"name" t::"trm" binds x in t
 binder
   bn::"assg \<Rightarrow> atom list"
 where

--- 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

--- a/Nominal/Ex/TypeSchemes.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -12,7 +12,7 @@
   Var "name"
 | Fun "ty" "ty"
 and tys =
-  All xs::"name fset" ty::"ty" bind (set+) xs in ty
+  All xs::"name fset" ty::"ty" binds (set+) xs in ty
 
 ML {*
 get_all_info @{context}
@@ -282,7 +282,7 @@
 | Fun2 "ty2" "ty2"
 
 nominal_datatype tys2 =
-  All2 xs::"name fset" ty::"ty2" bind (set+) xs in ty
+  All2 xs::"name fset" ty::"ty2" binds (set+) xs in ty
 
 thm tys2.distinct
 thm tys2.induct tys2.strong_induct

--- a/Nominal/Ex/TypeVarsTest.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/TypeVarsTest.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -20,9 +20,9 @@
 nominal_datatype ('a, 'b, 'c) lam =
   Var "name"
 | App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam"
-| Lam x::"name" l::"('a, 'b, 'c) lam"  bind x in l
+| Lam x::"name" l::"('a, 'b, 'c) lam"  binds x in l
 | Foo "'a" "'b"
-| Bar x::"'c" l::"('a, 'b, 'c) lam"  bind x in l   (* Bar binds a polymorphic atom *)
+| Bar x::"'c" l::"('a, 'b, 'c) lam"  binds x in l   (* Bar binds a polymorphic atom *)
 
 term Foo
 term Bar

--- a/Nominal/Ex/Weakening.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Weakening.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -9,7 +9,7 @@
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
-| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100,100] 100)
+| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100,100] 100)
 
 text {* Typing *}
 

--- a/Nominal/Nominal2.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Nominal2.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -679,13 +679,13 @@
   fun tuple3 ((x, y), (z, u)) = (x, y, z, u)
 in
 
-val _ = Keyword.keyword "bind"
+val _ = Keyword.keyword "binds"
 
 val opt_name = Scan.option (P.binding --| Args.colon)
 
 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
 
-val bind_mode = P.$$$ "bind" |--
+val bind_mode = P.$$$ "binds" |--
   S.optional (Args.parens 
     (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst