diff -r ba837d3ed37f -r 4b949985cf57 Nominal/ExLet.thy --- a/Nominal/ExLet.thy Thu Mar 25 15:06:58 2010 +0100 +++ b/Nominal/ExLet.thy Thu Mar 25 17:30:46 2010 +0100 @@ -7,6 +7,8 @@ atom_decl name ML {* val _ = recursive := false *} + + nominal_datatype trm = Vr "name" | Ap "trm" "trm"