--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Sep 26 10:00:59 2012 +0200
@@ -101,7 +101,7 @@
else rtac map_cong 1 THEN
EVERY' (map_index (fn (i, map_cong) =>
rtac map_cong THEN' EVERY' (map_index (fn (k, set_alt) =>
- EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac @{thm meta_mp},
+ EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac meta_mp,
rtac (equalityD2 RS set_mp), rtac (set_alt RS fun_cong RS trans),
rtac trans_o_apply, rtac (@{thm collect_def} RS arg_cong_Union),
rtac @{thm UnionI}, rtac @{thm UN_I}, REPEAT_DETERM_N i o rtac @{thm insertI2},