--- a/Quot/Nominal/Terms.thy	Thu Feb 18 10:00:58 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 18 10:01:48 2010 +0100
@@ -433,15 +433,14 @@
 | "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" [
+(*local_setup {* define_raw_fv "Terms.rtrm5" [
   [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]]  ] *}
-print_theorems
+print_theorems*)
 
 
 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}