--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Feb 10 16:46:21 2015 +0100
@@ -94,7 +94,7 @@
REPEAT_DETERM o (rtac (subset_UNIV RS conjI) ORELSE' etac conjI), atac] 1;
fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
- (EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN'
+ (EVERY' [rtac notI, hyp_subst_tac ctxt, forward_tac ctxt [alg_set]] THEN'
REPEAT_DETERM o FIRST'
[EVERY' [rtac @{thm subset_emptyI}, eresolve_tac ctxt wits],
EVERY' [rtac subsetI, rtac FalseE, eresolve_tac ctxt wits],