diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Classical.thy
--- 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