equal
deleted
inserted
replaced
7 text {* \solution{fun:revsum} *} |
7 text {* \solution{fun:revsum} *} |
8 |
8 |
9 ML {* |
9 ML {* |
10 fun rev_sum t = |
10 fun rev_sum t = |
11 let |
11 let |
12 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = |
12 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
13 u' :: dest_sum u |
|
14 | dest_sum u = [u] |
13 | dest_sum u = [u] |
15 in |
14 in |
16 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
15 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
17 end; |
16 end; |
18 *} |
17 *} |