author | desharna |
Thu, 06 Nov 2014 15:21:59 +0100 | |
changeset 58912 | 22928e3ba185 |
parent 58911 | 2cf595ee508b |
child 58913 | 5be251101978 |
--- 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;