src/Provers/Arith/cancel_numerals.ML
changeset 15531 08c8dad8e399
parent 15027 d23887300b96
child 15570 8d8c70b41bab
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -105,8 +105,8 @@
     1.4  	       (t', Data.mk_bal (Data.mk_sum T terms1', 
     1.5  				 newshape(n2-n1,terms2'))))
     1.6    end
     1.7 -  handle TERM _ => None
     1.8 -       | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
     1.9 +  handle TERM _ => NONE
    1.10 +       | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
    1.11  			     Undeclared type constructor "Numeral.bin"*)
    1.12  
    1.13  end;