use correct default for exclude rules to avoid weird tactic failures

--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:47:26 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:58:31 2014 +0100
@@ -1041,7 +1041,7 @@
         val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss);
         fun mk_excludesss excludes n =
           fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm])))
-            excludes (map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1));
+            excludes (map (fn k => replicate k [asm_rl] @ replicate (n - k) []) (0 upto n - 1));
         val excludessss =
           map2 (fn excludes => mk_excludesss excludes o length o #ctr_specs)
             (map2 append excludess' taut_thmss) corec_specs;