--- a/Nominal/Ex/SingleLet.thy Wed Jun 23 08:49:33 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Wed Jun 23 09:01:45 2010 +0200 @@ -4,8 +4,6 @@ atom_decl name -ML {* val _ = cheat_equivp := true *} - nominal_datatype trm = Var "name" | App "trm" "trm"