changeset 54742 | 7a86358a3c0b |
parent 53290 | b6c3be868217 |
child 54793 | c99f0fdb0886 |
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Fri Dec 13 23:53:02 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sat Dec 14 17:28:05 2013 +0100 @@ -567,7 +567,7 @@ EVERY' [rtac allI, fo_rtac induct ctxt, select_prem_tac n (dtac @{thm meta_spec2}) i, REPEAT_DETERM_N n o - EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac, + EVERY' [dtac meta_mp THEN_ALL_NEW Goal.norm_hhf_tac ctxt, REPEAT_DETERM o dtac @{thm meta_spec}, etac (spec RS meta_mp), atac], atac]; in