diff -r 6f43714517ee -r 08c8dad8e399 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Provers/Arith/cancel_numerals.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -105,8 +105,8 @@
 	       (t', Data.mk_bal (Data.mk_sum T terms1', 
 				 newshape(n2-n1,terms2'))))
   end
-  handle TERM _ => None
-       | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
+  handle TERM _ => NONE
+       | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
 			     Undeclared type constructor "Numeral.bin"*)
 
 end;