even more deads go to the end (continuation of e3a01b73579f)
authortraytel
Thu, 25 Sep 2014 09:01:14 +0200
changeset 58439 23124b918bfb
parent 58438 566117a31cc0
child 58440 07505e95db40
even more deads go to the end (continuation of e3a01b73579f)
src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 25 11:38:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 25 09:01:14 2014 +0200
@@ -607,7 +607,7 @@
     val ((kill_poss, _), (bnfs', ((_, unfold_set'), lthy'))) =
       normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum;
 
-    val Dss = map3 (append oo map o nth) livess kill_poss deadss;
+    val Dss = map3 (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
 
     fun pre_qualify b = Binding.qualify false (Binding.name_of b)
       #> not (Config.get lthy' bnf_note_all) ? Binding.conceal;