diff -r ad2feded2a8c -r 84baf466f2e3 Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Tue Feb 09 17:24:08 2010 +0100 +++ b/Quot/Nominal/Terms.thy Tue Feb 09 17:26:00 2010 +0100 @@ -926,11 +926,7 @@ done - - - - - +(* example with a bn function defined over the type itself *) datatype rtrm6 = rVr6 "name" | rAp6 "rtrm6" "rtrm6"