diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal/Ex/Classical.thy	Mon Jun 07 11:43:01 2010 +0200
@@ -11,12 +11,12 @@
 
 nominal_datatype trm =
    Ax "name" "coname"
-|  Cut n::"coname" t1::"trm" c::"coname" t2::"trm"              bind_set n in t1, bind_set c in t2
-|  AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname"  bind_set c1 in t1, bind_set c2 in t2
-|  AndL1 n::"name" t::"trm" "name"                              bind_set n in t
-|  AndL2 n::"name" t::"trm" "name"                              bind_set n in t
-|  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"        bind_set c in t1, bind_set n in t2
-|  ImpR c::"coname" n::"name" t::"trm" "coname"                 bind_set n c in t
+|  Cut n::"coname" t1::"trm" c::"coname" t2::"trm"             bind n in t1, bind c in t2
+|  AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2
+|  AndL1 n::"name" t::"trm" "name"                             bind n in t
+|  AndL2 n::"name" t::"trm" "name"                             bind n in t
+|  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"       bind c in t1, bind n in t2
+|  ImpR c::"coname" n::"name" t::"trm" "coname"                bind n c in t
 
 thm alpha_trm_raw.intros[no_vars]