--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Oct 06 11:50:23 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Oct 06 12:01:07 2015 +0200
@@ -357,8 +357,8 @@
val n = length card_of_min_algs;
in
EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
- REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp, rtac ctxt copy,
- REPEAT_DETERM_N n o assume_tac ctxt,
+ REPEAT_DETERM o dtac ctxt meta_spec, REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp,
+ rtac ctxt copy, REPEAT_DETERM_N n o assume_tac ctxt,
rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
rtac ctxt mor_comp, rtac ctxt mor_Rep, rtac ctxt mor_select, rtac ctxt CollectI, REPEAT_DETERM o rtac ctxt exI,
rtac ctxt conjI, rtac ctxt refl, assume_tac ctxt,