# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273673483 -7200
# Node ID 7c97467957675a9c4aef50f5d4a50b84adebce56
# Parent  287aa0d3d23af591b7b152d1bb853c79f5430121# Parent  502b1f3b282a48119d255ba85cded4f39ef31d62
merge

diff -r 287aa0d3d23a -r 7c9746795767 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Wed May 12 16:09:38 2010 +0200
+++ b/Nominal/Rsp.thy	Wed May 12 16:11:23 2010 +0200
@@ -62,8 +62,7 @@
 fun fvbv_rsp_tac induct fvbv_simps ctxt =
   rtac 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)