diff -r aead2aad845c -r 09bbed4f21d6 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Mon May 24 21:11:33 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Tue May 25 00:24:41 2010 +0100 @@ -5,7 +5,7 @@ atom_decl name ML {* print_depth 50 *} -declare [[STEPS = 5]] +declare [[STEPS = 8]] nominal_datatype trm =