# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266483708 -3600
# Node ID 3b24f33aedad5718703226e858a04b05b91322a9
# Parent  166cc41091b9306756c9847958522d2d9380b6df
Changed back to original version of trm5

diff -r 166cc41091b9 -r 3b24f33aedad Quot/Nominal/Terms.thy
--- 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"] *}