--- a/Nominal/Term5.thy	Mon Mar 22 15:27:01 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 22 17:21:27 2010 +0100
@@ -183,7 +183,7 @@
 local_setup {* snd o Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel @{context} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases}) [(@{thms rtrm5.distinct}, @{term alpha_rtrm5}), (@{thms rlts.distinct}, @{term alpha_rlts}), (@{thms rlts.distinct}, @{term alpha_rbv5})]))) *}
 print_theorems
 
-local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *}
+local_setup {* snd o Local_Theory.note ((@{binding alpha_bn_rsp}, []), prove_alpha_bn_rsp [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts} @{thms rtrm5.exhaust rlts.exhaust} @{thms alpha5_inj alpha_dis} @{thms alpha5_equivp} @{context} (@{term alpha_rbv5}, 1)) *}
 thm alpha_bn_rsp
 
 lemma [quot_respect]:
@@ -203,6 +203,7 @@
   apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
 done
 
+
 lemma
   shows "(alpha_rlts ===> op =) rbv5 rbv5"
   by (simp add: bv_list_rsp)