# HG changeset patch
# User desharna
# Date 1415283719 -3600
# Node ID 22928e3ba18518ab1dd23a17bbe33a1fb74159f7
# Parent  2cf595ee508b3931d1f74822f3dca09d18dbe1de
fix 'unfla' function

diff -r 2cf595ee508b -r 22928e3ba185 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Nov 05 20:59:24 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Nov 06 15:21:59 2014 +0100
@@ -424,7 +424,7 @@
       | zed xs (y :: ys) = f (xs, y, ys) :: zed (xs @ [y]) ys;
   in zed [] end;
 
-fun unfla _ = rpair [];
+fun unfla xss = fold_map (fn _ => fn (c :: cs) => (c,cs)) xss;
 fun unflat xss = fold_map unfla xss;
 fun unflatt xsss = fold_map unflat xsss;
 fun unflattt xssss = fold_map unflatt xssss;