# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273673463 -7200
# Node ID 502b1f3b282a48119d255ba85cded4f39ef31d62
# Parent  409ecb7284dd44b8a82783fdd05a8e0e7b18749e
fvbv_rsp include prod_rel.simps

diff -r 409ecb7284dd -r 502b1f3b282a Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Wed May 12 13:43:48 2010 +0100
+++ b/Nominal/Rsp.thy	Wed May 12 16:11:03 2010 +0200
@@ -62,8 +62,7 @@
 fun fvbv_rsp_tac induct fvbv_simps ctxt =
   rel_indtac induct THEN_ALL_NEW
   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas prod_rel.simps prod_fv.simps} @ fvbv_simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms prod_fv.simps prod_rel.simps alphas} @ fvbv_simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
   TRY o blast_tac (claset_of ctxt)