# HG changeset patch
# User blanchet
# Date 1389362311 -3600
# Node ID d1c76303244eb37eda750ac6349544edb85d837d
# Parent  b35859240103eb44204e872f44f29c3b5bdbf52b
use correct default for exclude rules to avoid weird tactic failures

diff -r b35859240103 -r d1c76303244e src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- 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;