src/Provers/Arith/combine_numerals.ML
changeset 15531 08c8dad8e399
parent 15027 d23887300b96
child 15570 8d8c70b41bab
--- a/src/Provers/Arith/combine_numerals.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Provers/Arith/combine_numerals.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -47,21 +47,21 @@
       raise TERM("combine_numerals: remove", [])  
   | remove (m, u, t::terms) =
       case try Data.dest_coeff t of
-	  Some(n,v) => if m=n andalso u aconv v then terms
+	  SOME(n,v) => if m=n andalso u aconv v then terms
 		       else t :: remove (m, u, terms)
-	| None      =>  t :: remove (m, u, terms);
+	| NONE      =>  t :: remove (m, u, terms);
 
 (*a left-to-right scan of terms, seeking another term of the form #n*u, where
   #m*u is already in terms for some m*)
 fun find_repeated (tab, _, []) = raise TERM("find_repeated", []) 
   | find_repeated (tab, past, t::terms) =
       case try Data.dest_coeff t of
-	  Some(n,u) => 
+	  SOME(n,u) => 
 	      (case Termtab.lookup (tab, u) of
-		  Some m => (u, m, n, rev (remove (m,u,past)) @ terms)
-		| None => find_repeated (Termtab.update ((u,n), tab), 
+		  SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
+		| NONE => find_repeated (Termtab.update ((u,n), tab), 
 					 t::past,  terms))
-	| None => find_repeated (tab, t::past, terms);
+	| NONE => find_repeated (tab, t::past, terms);
 
 (*the simplification procedure*)
 fun proc sg _ t =
@@ -84,8 +84,8 @@
 	     Data.numeral_simp_tac] sg xs
 	    (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
   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;