--- a/Quot/Nominal/LFex.thy	Wed Feb 24 10:25:59 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 10:38:45 2010 +0100
@@ -72,23 +72,23 @@
 and alpha_rty    ("_ \<approx>ty _" [100, 100] 100)
 and alpha_rtrm   ("_ \<approx>tr _" [100, 100] 100)
 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *}
-thm alphas_inj
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_rkind_alpha_rty_alpha_rtrm_inj}, []), (build_alpha_inj @{thms alpha_rkind_alpha_rty_alpha_rtrm.intros} @{thms rkind.distinct rty.distinct rtrm.distinct rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases} ctxt)) ctxt)) *}
+thm alpha_rkind_alpha_rty_alpha_rtrm_inj
 
-lemma alphas_eqvt:
+lemma alpha_eqvt:
   "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
-  "t2 \<approx>rty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>rty (pi \<bullet> s2)"
+  "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
   "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
 sorry
 
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alphas_equivp}, []),
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []),
   (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}]
      @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} 
-     @{thms rkind.inject rty.inject rtrm.inject} @{thms alphas_inj}
+     @{thms rkind.inject rty.inject rtrm.inject} @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}
      @{thms rkind.distinct rty.distinct rtrm.distinct}
      @{thms alpha_rkind.cases alpha_rty.cases alpha_rtrm.cases}
-     @{thms alphas_eqvt} ctxt)) ctxt)) *}
-thm alphas_equivp
+     @{thms alpha_eqvt} ctxt)) ctxt)) *}
+thm alpha_equivps
 *)
 
 primrec