diff -r 811c35e81ac5 -r 8601434fa334 src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- 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),