# HG changeset patch
# User blanchet
# Date 1347408391 -7200
# Node ID 30916e44d8282d5be6febdea4776601432940f32
# Parent  c13fff97a8df3c23d95aaca121bdf5007f94b738
tuning

diff -r c13fff97a8df -r 30916e44d828 src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML
--- 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,