tuned code to allow mutualized corecursion through different functions with the same target type
authorblanchet
Fri, 14 Feb 2014 16:21:41 +0100
changeset 55483 f223445a4d0c
parent 55482 61ffc2339a8c
child 55484 9deb5066508f
tuned code to allow mutualized corecursion through different functions with the same target type
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