diff -r 93ab397f5980 -r 86c977b4a9bb Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Tue Jun 01 15:01:05 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Tue Jun 01 15:21:01 2010 +0200 @@ -7,7 +7,7 @@ ML {* Function.add_function *} ML {* print_depth 50 *} -declare [[STEPS = 8]] +declare [[STEPS = 9]] nominal_datatype trm =