diff -r 6f43714517ee -r 08c8dad8e399 src/Provers/Arith/extract_common_term.ML
--- a/src/Provers/Arith/extract_common_term.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Provers/Arith/extract_common_term.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -70,8 +70,8 @@
   in
       apsome Data.simplify_meta_eq reshape
   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;