--- a/Nominal/Ex/SingleLet.thy Fri May 21 11:40:18 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Sat May 22 13:51:47 2010 +0100 @@ -7,6 +7,7 @@ ML {* print_depth 50 *} declare [[STEPS = 4]] + nominal_datatype trm = Var "name" | App "trm" "trm"