55 #m*u is already in terms for some m*) |
55 #m*u is already in terms for some m*) |
56 fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) |
56 fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) |
57 | find_repeated (tab, past, t::terms) = |
57 | find_repeated (tab, past, t::terms) = |
58 case try Data.dest_coeff t of |
58 case try Data.dest_coeff t of |
59 SOME(n,u) => |
59 SOME(n,u) => |
60 (case Termtab.curried_lookup tab u of |
60 (case Termtab.lookup tab u of |
61 SOME m => (u, m, n, rev (remove (m,u,past)) @ terms) |
61 SOME m => (u, m, n, rev (remove (m,u,past)) @ terms) |
62 | NONE => find_repeated (Termtab.curried_update (u, n) tab, |
62 | NONE => find_repeated (Termtab.update (u, n) tab, |
63 t::past, terms)) |
63 t::past, terms)) |
64 | NONE => find_repeated (tab, t::past, terms); |
64 | NONE => find_repeated (tab, t::past, terms); |
65 |
65 |
66 (*the simplification procedure*) |
66 (*the simplification procedure*) |
67 fun proc thy ss t = |
67 fun proc thy ss t = |