# HG changeset patch
# User traytel
# Date 1410440936 -7200
# Node ID e3a01b73579fc2f74f9191e5e61862dd7455574b
# Parent  759e47518d80a3e0f7ae3a6b98104768977937b6
new deads go to the end

diff -r 759e47518d80 -r e3a01b73579f src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Sep 11 11:49:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Sep 11 15:08:56 2014 +0200
@@ -435,7 +435,7 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (killedAs @ Ds))
+      bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (Ds @ killedAs))
         Binding.empty Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
@@ -667,7 +667,7 @@
     val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) =
       normalize_bnfs qualify Ass Ds sort inners accum;
 
-    val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
+    val Ds = oDs @ flat (map3 (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
     val As = map TFree As;
   in
     apfst (rpair (Ds, As))