diff -r 43bd70786f9f -r 0f92257edeee Quot/Nominal/Fv.thy
--- 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
 *}