--- a/Quot/Nominal/Fv.thy	Mon Feb 22 16:16:04 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 16:44:58 2010 +0100
@@ -253,17 +253,17 @@
 *}
 
 ML {*
-fun build_alpha_refl_gl alphas =
+fun build_alpha_refl_gl alphas (x, y, z) =
 let
   fun build_alpha alpha =
     let
       val ty = domain_type (fastype_of alpha);
-      val var = Free("x", ty);
-      val var2 = Free("y", ty);
-      val var3 = Free("z", ty);
+      val var = Free(x, ty);
+      val var2 = Free(y, ty);
+      val var3 = Free(z, ty);
       val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
       val transp = HOLogic.mk_imp (alpha $ var $ var2,
-        HOLogic.mk_all ("z", ty,
+        HOLogic.mk_all (z, ty,
           HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
     in
       ((alpha $ var $ var), (symp, transp))
@@ -307,17 +307,23 @@
 *}
 
 ML {*
-fun build_equivps alphas induct alpha_inj term_inj distinct cases eqvt ctxt =
+fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
 let
-  val (reflg, (symg, transg)) = build_alpha_refl_gl alphas
-  fun reflp_tac' _ = reflp_tac induct term_inj 1;
-  fun symp_tac' _ = symp_tac induct alpha_inj eqvt 1;
-  fun transp_tac' _ = transp_tac induct alpha_inj term_inj distinct cases eqvt 1;
-  val reflt = Goal.prove ctxt ["x"] [] reflg reflp_tac';
-  val symt = Goal.prove ctxt ["x","y"] [] symg symp_tac';
-  val transt = Goal.prove ctxt ["x","y","z"] [] transg transp_tac';
+  val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt;
+  val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z)
+  fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1;
+  fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1;
+  fun transp_tac' _ = transp_tac alpha_induct alpha_inj term_inj distinct cases eqvt 1;
+  val reflt = Goal.prove ctxt' [] [] reflg reflp_tac';
+  val symt = Goal.prove ctxt' [] [] symg symp_tac';
+  val transt = Goal.prove ctxt' [] [] transg transp_tac';
+  val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt]
+  fun equivp alpha =
+    let
+      val goal = @{term Trueprop} $ (@{term equivp} $ alpha)
+      val tac = 
 in
-  (reflt, symt, transt)
+  (refltg, symtg, transtg)
 end
 *}
 

--- a/Quot/Nominal/Terms.thy	Mon Feb 22 16:16:04 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 16:44:58 2010 +0100
@@ -116,33 +116,37 @@
   apply(simp add: permute_eqvt[symmetric])
   done
 
-
+ML {*
+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} @{context}
+*}
+ML Variable.export
 
-prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
+prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
 by (tactic {* reflp_tac @{thm rtrm1_bp.induct} @{thms alpha1_inj} 1 *})
 
-prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
+prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms alpha1_eqvt} 1 *})
 
-prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
+prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}] ("x","y","z")) *}
 by (tactic {* transp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} @{thms rtrm1.inject bp.inject} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} 1 *})
 
-lemma helper: "(\<forall>x y z. R x y \<and> R y z \<longrightarrow> R x z) = (\<forall>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z))"
-by meson
+lemma transp_aux:
+  "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R"
+  unfolding transp_def
+  by blast
 
 lemma alpha1_equivp:
   "equivp alpha_rtrm1"
   "equivp alpha_bp"
-unfolding equivp_reflp_symp_transp reflp_def
-apply (simp_all add: alpha1_reflp_aux)
-unfolding symp_def
-apply (simp_all add: alpha1_symp_aux)
-unfolding transp_def
-apply (simp_all only: helper)
-apply (rule allI)+
-apply (rule conjunct1[OF alpha1_transp_aux])
-apply (rule allI)+
-apply (rule conjunct2[OF alpha1_transp_aux])
+apply (tactic {*
+  (simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def})
+  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN'
+  resolve_tac (HOLogic.conj_elims @{thm alpha1_reflp_aux})
+  THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'
+  resolve_tac (HOLogic.conj_elims @{thm alpha1_symp_aux}) THEN' rtac @{thm transp_aux}
+  THEN' resolve_tac (HOLogic.conj_elims @{thm alpha1_transp_aux})
+)
+1 *})
 done
 
 quotient_type trm1 = rtrm1 / alpha_rtrm1
@@ -526,13 +530,13 @@
   apply (simp)
   done
 
-prove alpha5_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *}
+prove alpha5_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *}
 by (tactic {* reflp_tac @{thm rtrm5_rlts.induct} @{thms alpha5_inj} 1 *})
 
-prove alpha5_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *}
+prove alpha5_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *}
 by (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} 1 *})
 
-prove alpha5_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}]) *}
+prove alpha5_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm5}, @{term alpha_rlts}] ("x","y","z")) *}
 by (tactic {* transp_tac @{thm alpha_rtrm5_alpha_rlts.induct} @{thms alpha5_inj} @{thms rtrm5.inject rlts.inject} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} 1 *})
 
 lemma alpha5_equivps: