| changeset 58912 | 22928e3ba185 |
| parent 58734 | 20235f0512e2 |
| child 58935 | dcad9bad43e7 |
--- 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;