# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273673884 -7200
# Node ID af11e9fbc45af5eb229638978fd8207d1a3d7749
# Parent  7c97467957675a9c4aef50f5d4a50b84adebce56# Parent  872187804ff57e74a8c0cfc7a975f801b44361c3
merge

diff -r 872187804ff5 -r af11e9fbc45a Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Wed May 12 15:17:35 2010 +0100
+++ b/Nominal/Rsp.thy	Wed May 12 16:18:04 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)