--- a/Quot/Nominal/Fv.thy	Mon Feb 22 16:44:58 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 17:19:28 2010 +0100
@@ -288,7 +288,7 @@
 
 ML {*
 fun symp_tac induct inj eqvt =
-  rtac induct THEN_ALL_NEW
+  ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
   TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
   (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt)
@@ -296,7 +296,7 @@
 
 ML {*
 fun transp_tac induct alpha_inj term_inj distinct cases eqvt =
-  rtac induct THEN_ALL_NEW
+  ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
   (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN'
   eresolve_tac cases) THEN_ALL_NEW
   (
@@ -306,6 +306,21 @@
   )
 *}
 
+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
+
+ML {*
+fun equivp_tac reflps symps transps =
+  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 reflps THEN'
+  rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN'
+  resolve_tac symps THEN'
+  rtac @{thm transp_aux} THEN' resolve_tac transps
+*}
+
 ML {*
 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt =
 let
@@ -318,12 +333,19 @@
   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]
+  val reflts = HOLogic.conj_elims refltg
+  val symts = HOLogic.conj_elims symtg
+  val transts = HOLogic.conj_elims transtg
   fun equivp alpha =
     let
-      val goal = @{term Trueprop} $ (@{term equivp} $ alpha)
-      val tac = 
+      val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool})
+      val goal = @{term Trueprop} $ (equivp $ alpha)
+      fun tac _ = equivp_tac reflts symts transts 1
+    in
+      Goal.prove ctxt [] [] goal tac
+    end
 in
-  (refltg, symtg, transtg)
+  map equivp alphas
 end
 *}