# HG changeset patch
# User blanchet
# Date 1389361646 -3600
# Node ID b35859240103eb44204e872f44f29c3b5bdbf52b
# Parent  5747fdd4ad3b8cb4b0a8afe24e2e8e7eaa8205d0
tuning (no need for |-> here)

diff -r 5747fdd4ad3b -r b35859240103 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:39:37 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Fri Jan 10 14:47:26 2014 +0100
@@ -1040,11 +1040,11 @@
 
         val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss);
         fun mk_excludesss excludes n =
-          (excludes, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1))
-          |-> fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm])));
-        val excludessss = (excludess' ~~ taut_thmss |> map (op @), fun_names ~~ corec_specs)
-          |-> map2 (fn excludes => fn (_, {ctr_specs, ...}) =>
-            mk_excludesss excludes (length ctr_specs));
+          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));
+        val excludessss =
+          map2 (fn excludes => mk_excludesss excludes o length o #ctr_specs)
+            (map2 append excludess' taut_thmss) corec_specs;
 
         fun prove_disc ({ctr_specs, ...} : corec_spec) excludesss
             ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =