--- a/Nominal/Fv.thy	Thu Mar 04 11:16:36 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 04 12:00:11 2010 +0100
@@ -184,8 +184,8 @@
               val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;
               val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"})
             in
-              if length pi_supps > 1 then
-                HOLogic.mk_conj (alpha_gen, pi_supps_eq) else alpha_gen
+              (*if length pi_supps > 1 then
+                HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) alpha_gen
             (* TODO Add some test that is makes sense *)
             end else @{term "True"}
         end
@@ -372,17 +372,38 @@
 by auto
 
 ML {*
+fun is_ex (Const ("Ex", _) $ Abs _) = true
+  | is_ex _ = false;
+*}
+
+ML {*
+fun eetac rule = Subgoal.FOCUS_PARAMS 
+  (fn (focus) =>
+     let
+       val concl = #concl focus
+       val prems = Logic.strip_imp_prems (term_of concl)
+       val exs = filter (fn x => is_ex (HOLogic.dest_Trueprop x)) prems
+       val cexs = map (SOME o (cterm_of (ProofContext.theory_of (#context focus)))) exs
+       val thins = map (fn cex => Drule.instantiate' [] [cex] Drule.thin_rl) cexs
+     in
+     (etac rule THEN' RANGE[
+        atac,
+        eresolve_tac thins
+     ]) 1
+     end
+  )
+*}
+
+ML {*
 fun transp_tac ctxt induct alpha_inj term_inj distinct cases eqvt =
-  ((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
+  ind_tac induct THEN_ALL_NEW
   (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW
-  (
-    asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct)
-    THEN_ALL_NEW (REPEAT o etac conjE THEN' etac @{thm exi_sum} THEN' RANGE [atac]) THEN_ALL_NEW
-    (REPEAT o etac conjE THEN' (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)))
-    THEN_ALL_NEW (asm_full_simp_tac HOL_ss) THEN_ALL_NEW
-    (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW
-    (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt)))
-  )
+  asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW
+  split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conjs
+  THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
+  THEN_ALL_NEW split_conjs THEN_ALL_NEW
+  TRY o (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW
+  (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
 *}
 
 lemma transp_aux:

--- a/Nominal/Parser.thy	Thu Mar 04 11:16:36 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 04 12:00:11 2010 +0100
@@ -248,15 +248,15 @@
   val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms
     (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6;
   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
-(*  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
+  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
     inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6;
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
   val qty_names = map (fn (_, b, _, _) => b) dts;
   val lthy7 = define_quotient_type
     (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_names ~~ all_typs) ~~ alpha_ts))
-    (ALLGOALS (resolve_tac alpha_equivp)) lthy6;*)
+    (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
 in
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy6)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy7)
 end
 *}