--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Jan 12 13:16:00 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Jan 12 14:32:22 2014 +0100
@@ -782,7 +782,7 @@
fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} =
let val n = length ks;
in
- unfold_tac @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} ctxt THEN
+ unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong =>
EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),