diff -r 02b24877be3e -r e6e6a3da81aa Nominal/Ex/SystemFOmega.thy --- 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 = - \ | KFun kind kind + \ +| 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