removed dead code: listof;
authorwenzelm
Fri, 05 May 2000 22:32:49 +0200
changeset 8816 31b4fb3d8d60
parent 8815 187547eae4c5
child 8817 1c48b3732399
removed dead code: listof;
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", [])