--- 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;