diff -r 187547eae4c5 -r 31b4fb3d8d60 src/Provers/Arith/combine_numerals.ML
--- 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", [])