--- a/Nominal/Term4.thy	Tue Mar 02 08:58:28 2010 +0100
+++ b/Nominal/Term4.thy	Tue Mar 02 11:04:49 2010 +0100
@@ -30,7 +30,7 @@
 thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
 
 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term4.rtrm4")
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}
+  [[[], [], [(NONE, 0,1)]], [[], []]  ] *}
 print_theorems
 
 notation