--- a/Quot/Nominal/Terms.thy	Thu Feb 18 09:46:38 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 18 10:00:58 2010 +0100
@@ -432,9 +432,17 @@
   "rbv5 rLnil = {}"
 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
 
+
+(*
 local_setup {* define_raw_fv "Terms.rtrm5" [
   [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ] *}
 print_theorems
+*)
+(* Alternate version with additional binding of name in rlts in rLcons *)
+local_setup {* define_raw_fv "Terms.rtrm5" [
+  [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]]  ] *}
+print_theorems
+
 
 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}
 print_theorems