# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272893841 -7200
# Node ID e72121ea134b693b3282e675a7cbe99d0a411765
# Parent  15c5a29266225e1e0078ba989d6dbe1e4f055db2
alpha_eqvt_tac fixed to work when the existential is not at the top level.

diff -r 15c5a2926622 -r e72121ea134b Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Mon May 03 15:36:47 2010 +0200
+++ b/Nominal/Rsp.thy	Mon May 03 15:37:21 2010 +0200
@@ -97,7 +97,7 @@
 ML {*
 fun alpha_eqvt_tac induct simps ctxt =
   rel_indtac induct THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps