--- a/Nominal/Term1.thy	Thu Feb 25 14:14:40 2010 +0100
+++ b/Nominal/Term1.thy	Thu Feb 25 15:40:09 2010 +0100
@@ -74,6 +74,7 @@
   apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"])
   apply (simp_all only: alpha1_eqvt)
 done
+thm eqvts_raw(1)
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
   (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}