--- a/LamEx.thy	Wed Nov 04 16:10:39 2009 +0100
+++ b/LamEx.thy	Thu Nov 05 09:38:34 2009 +0100
@@ -165,6 +165,12 @@
 lemma rfv_rsp: "(alpha ===> op =) rfv rfv"
   sorry
 
+lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
+apply (auto)
+apply (erule alpha.cases)
+apply (simp_all add: rlam.inject alpha_refl)
+done
+
 ML {* val qty = @{typ "lam"} *}
 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *}
 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @
@@ -187,6 +193,8 @@
 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *}
 
+ML {* val var_inject = lift_thm_lam @{context} @{thm rvar_inject} *}
+
 local_setup {*
   Quotient.note (@{binding "pi_var"}, pi_var) #> snd #>
   Quotient.note (@{binding "pi_app"}, pi_app) #> snd #>
@@ -195,7 +203,8 @@
   Quotient.note (@{binding "a2"}, a2) #> snd #>
   Quotient.note (@{binding "a3"}, a3) #> snd #>
   Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd #>
-  Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd
+  Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd #>
+  Quotient.note (@{binding "var_inject"}, var_inject) #> snd
 *}
 
 thm alpha.cases
@@ -203,18 +212,6 @@
 thm alpha.induct
 thm alpha_induct
 
-lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
-apply (auto)
-apply (erule alpha.cases)
-apply (simp_all add: rlam.inject alpha_refl)
-done
-
-ML {* val var_inject = Toplevel.program (fn () => lift_thm_lam @{context} @{thm rvar_inject}) *}
-
-local_setup {*
-  Quotient.note (@{binding "var_inject"}, var_inject) #> snd
-*}
-
 lemma var_supp:
   shows "supp (Var a) = ((supp a)::name set)"
   apply(simp add: supp_def)