equal
deleted
inserted
replaced
28 | mk_sum plus tms = foldr1 (fn (x, y) => plus $ x $ y) tms; |
28 | mk_sum plus tms = foldr1 (fn (x, y) => plus $ x $ y) tms; |
29 |
29 |
30 (*Separate the literals from the other terms being combined*) |
30 (*Separate the literals from the other terms being combined*) |
31 fun sift_terms plus (t, (lits,others)) = |
31 fun sift_terms plus (t, (lits,others)) = |
32 (case t of |
32 (case t of |
33 Const (@{const_name Numeral.number_of}, _) $ _ => (* FIXME logic dependent *) |
33 Const (@{const_name Int.number_of}, _) $ _ => (* FIXME logic dependent *) |
34 (t::lits, others) (*new literal*) |
34 (t::lits, others) (*new literal*) |
35 | (f as Const _) $ x $ y => |
35 | (f as Const _) $ x $ y => |
36 if f = plus |
36 if f = plus |
37 then sift_terms plus (x, sift_terms plus (y, (lits,others))) |
37 then sift_terms plus (x, sift_terms plus (y, (lits,others))) |
38 else (lits, t::others) (*arbitrary summand*) |
38 else (lits, t::others) (*arbitrary summand*) |