diff -r 892fcdb96c96 -r aeed597d2043 Nominal/LFex.thy --- a/Nominal/LFex.thy Tue Mar 23 08:22:48 2010 +0100 +++ b/Nominal/LFex.thy Tue Mar 23 08:33:48 2010 +0100 @@ -5,8 +5,6 @@ atom_decl name atom_decl ident -ML {* val _ = cheat_equivp := false *} - nominal_datatype kind = Type | KPi "ty" n::"name" k::"kind" bind n in k