changeset 15531 | 08c8dad8e399 |
parent 15027 | d23887300b96 |
child 15570 | 8d8c70b41bab |
--- 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;