--- a/Nominal/Ex/Ex2.thy Mon May 03 15:37:21 2010 +0200 +++ b/Nominal/Ex/Ex2.thy Mon May 03 15:38:20 2010 +0200 @@ -6,8 +6,6 @@ atom_decl name -ML {* val _ = cheat_alpha_eqvt := true *} - nominal_datatype trm = Var "name" | App "trm" "trm"