author | wenzelm |
Fri, 05 May 2000 22:32:49 +0200 | |
changeset 8816 | 31b4fb3d8d60 |
parent 8815 | 187547eae4c5 |
child 8817 | 1c48b3732399 |
--- a/src/Provers/Arith/combine_numerals.ML Fri May 05 22:32:25 2000 +0200 +++ b/src/Provers/Arith/combine_numerals.ML Fri May 05 22:32:49 2000 +0200 @@ -41,9 +41,6 @@ = struct -fun listof None = [] - | listof (Some x) = [x]; - (*Remove the first occurrence of #m*u from the term list*) fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*) raise TERM("combine_numerals: remove", [])