# HG changeset patch
# User blanchet
# Date 1392391301 -3600
# Node ID f223445a4d0c3a3f70499f37749ddd56366b16e0
# Parent  61ffc2339a8cc7e92c295a8b3b3079d01bd3bca2
tuned code to allow mutualized corecursion through different functions with the same target type

diff -r 61ffc2339a8c -r f223445a4d0c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 15:39:43 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 16:21:41 2014 +0100
@@ -874,7 +874,7 @@
           let val T = fastype_of cqf in
             if exists_subtype_in Cs T then
               let val U = mk_U maybe_mk_sumT T in
-                build_map lthy (indexify snd fpTs (fn kk => fn _ =>
+                build_map lthy (indexify fst (map2 maybe_mk_sumT fpTs Cs) (fn kk => fn _ =>
                   maybe_tack (nth cs kk, nth us kk) (nth fcoiters kk))) (T, U) $ cqf
               end
             else