--- a/Nominal/Test.thy	Mon Mar 01 16:55:41 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 01 19:23:08 2010 +0100
@@ -40,7 +40,7 @@
 where 
   "f PN = {}"
 | "f (PS x) = {x}"
-| "f (PD x y) = {x,y}"
+| "f (PD x y) = {x, y}"
 
 thm f_raw.simps
 
@@ -78,7 +78,7 @@
 nominal_datatype trm1 =
   Vr1 "name"
 | Ap1 "trm1" "trm1"
-| Lm1 x::"name" t::"trm1"      bind x in t 
+| Lm1 x::"name" t::"trm1"       bind x in t 
 | Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t 
 and bp1 =
   BUnit1
@@ -203,13 +203,13 @@
 atom_decl coname
 
 nominal_datatype phd =
-   Ax name coname
-|  Cut n::name t1::phd c::coname t2::phd               bind n in t1, bind c in t2
-|  AndR c1::coname t1::phd c2::coname t2::phd coname   bind c1 in t1, bind c2 in t2
-|  AndL1 n::name t::phd name                           bind n in t
-|  AndL2 n::name t::phd name                           bind n in t
-|  ImpL c::coname t1::phd n::name t2::phd name         bind c in t1, bind n in t2
-|  ImpR c::coname n::name t::phd coname                bind n in 1, bind c in t
+   Ax "name" "coname"
+|  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
+|  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
+|  AndL1 n::"name" t::"phd" "name"                              bind n in t
+|  AndL2 n::"name" t::"phd" "name"                              bind n in t
+|  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
+|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in 1, bind c in t
 
 (* example form Leroy 96 about modules; OTT *)