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