equal
deleted
inserted
replaced
38 sig |
38 sig |
39 val proc: Sign.sg -> thm list -> term -> thm option |
39 val proc: Sign.sg -> thm list -> term -> thm option |
40 end |
40 end |
41 = |
41 = |
42 struct |
42 struct |
43 |
|
44 fun listof None = [] |
|
45 | listof (Some x) = [x]; |
|
46 |
43 |
47 (*Remove the first occurrence of #m*u from the term list*) |
44 (*Remove the first occurrence of #m*u from the term list*) |
48 fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*) |
45 fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*) |
49 raise TERM("combine_numerals: remove", []) |
46 raise TERM("combine_numerals: remove", []) |
50 | remove (m, u, t::terms) = |
47 | remove (m, u, t::terms) = |