src/Provers/Arith/combine_numerals.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15965 f422f8283491
--- a/src/Provers/Arith/combine_numerals.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/Provers/Arith/combine_numerals.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -78,7 +78,7 @@
 			 Data.mk_sum T ([Data.mk_coeff(m,u),
 				         Data.mk_coeff(n,u)] @ terms))
   in
-      apsome Data.simplify_meta_eq
+      Option.map Data.simplify_meta_eq
 	 (Data.prove_conv 
 	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
 	     Data.numeral_simp_tac] sg xs