--- a/Nominal/Manual/Term4.thy	Wed May 12 16:33:50 2010 +0100
+++ b/Nominal/Manual/Term4.thy	Wed May 12 16:59:53 2010 +0100
@@ -65,6 +65,8 @@
 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
   build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms perm_fixed alpha4_inj} ctxt 1) ctxt) ctxt))
 *}
+
+
 thm alpha4_eqvt
 lemmas alpha4_eqvt_fixed = alpha4_eqvt(1)[simplified alpha_fix (*fv_fix*)]