--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Wed Sep 12 02:05:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Wed Sep 12 02:06:31 2012 +0200
@@ -826,7 +826,7 @@
(rev (active_set_naturals ~~ in_Irels))])
(set_simps ~~ passive_set_naturals),
rtac conjI,
- REPEAT_DETERM_N 2 o EVERY'[rtac trans, rtac map_simp, rtac (fld_inject RS iffD2),
+ REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac map_simp, rtac (fld_inject RS iffD2),
rtac trans, rtac map_comp, rtac trans, rtac map_cong,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,