--- a/Nominal/Ex/SystemFOmega.thy	Wed Dec 22 21:13:32 2010 +0000
+++ b/Nominal/Ex/SystemFOmega.thy	Wed Dec 22 21:13:44 2010 +0000
@@ -13,7 +13,8 @@
 atom_decl label
 
 nominal_datatype kind =
-  \<Omega> | KFun kind kind
+  \<Omega> 
+| KFun kind kind
 
 nominal_datatype ty =
   TVar tvar
@@ -41,7 +42,6 @@
   RNil
 | RCons label trm rec
 
-
 thm ty_trec.distinct
 thm ty_trec.induct
 thm ty_trec.inducts