--- a/Nominal/Rsp.thy	Mon Mar 22 15:27:01 2010 +0100
+++ b/Nominal/Rsp.thy	Mon Mar 22 17:21:27 2010 +0100
@@ -270,34 +270,37 @@
   by blast
 
 ML {*
-fun prove_alpha_bn_rsp alphas inducts inj_dis equivps ctxt (alpha_bn, n) =
+fun prove_alpha_bn_rsp alphas inducts exhausts inj_dis equivps ctxt (alpha_bn, n) =
 let
   val alpha = nth alphas n;
   val ty = domain_type (fastype_of alpha);
-  val names = Datatype_Prop.make_tnames [ty, ty];
-  val [l, r] = map (fn x => (Free (x, ty))) names;
+  val ([x, y, a], ctxt') = Variable.variant_fixes ["x","y","a"] ctxt;
+  val [l, r] = map (fn x => (Free (x, ty))) [x, y]
+  val lhs = HOLogic.mk_Trueprop (alpha $ l $ r)
   val g1 =
-    Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r),
-      HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty,
-        HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0))))
+    Logic.mk_implies (lhs,
+      HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty,
+        HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0))));
   val g2 =
-    Logic.mk_implies (HOLogic.mk_Trueprop (alpha $ l $ r),
-      HOLogic.mk_Trueprop (HOLogic.mk_all ("a", ty,
-        HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))))
+    Logic.mk_implies (lhs,
+      HOLogic.mk_Trueprop (HOLogic.mk_all (a, ty,
+        HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))));
+  val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;
+  val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;
   fun tac {context, ...} = (
     etac (nth inducts n) THEN_ALL_NEW
     (TRY o rtac @{thm TrueI}) THEN_ALL_NEW rtac allI THEN_ALL_NEW
-    InductTacs.case_tac context "a" THEN_ALL_NEW split_conjs THEN_ALL_NEW
+    split_conjs THEN_ALL_NEW
+    InductTacs.case_rule_tac context a (nth exhausts n) THEN_ALL_NEW
     asm_full_simp_tac (HOL_ss addsimps inj_dis) THEN_ALL_NEW
-    REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
-    TRY o eresolve_tac (map (fn x => @{thm equivp_rspl} OF [x]) equivps) THEN_ALL_NEW
-    TRY o eresolve_tac (map (fn x => @{thm equivp_rspr} OF [x]) equivps) THEN_ALL_NEW
-    TRY o rtac refl
+    TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
+    TRY o eresolve_tac (resl @ resr) THEN_ALL_NEW
+    asm_full_simp_tac (HOL_ss addsimps inj_dis)
   ) 1;
-  val t1 = Goal.prove ctxt names [] g1 tac;
-  val t2 = Goal.prove ctxt names [] g2 tac;
+  val t1 = Goal.prove ctxt [] [] g1 tac;
+  val t2 = Goal.prove ctxt [] [] g2 tac;
 in
-  [t1, t2]
+  Variable.export ctxt' ctxt [t1, t2]
 end
 *}