src/Provers/Arith/cancel_numerals.ML
changeset 8772 ebb07113c4f7
parent 8760 9139453d7033
child 8779 2d4afbc46801
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Tue Apr 25 08:09:10 2000 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Fri Apr 28 10:44:03 2000 +0200
     1.3 @@ -81,10 +81,13 @@
     1.4        fun newshape (i,terms) = Data.mk_sum (Data.mk_coeff(i,u)::terms)
     1.5        val reshapes =  (*Move i*u to the front and put j*u into standard form
     1.6  		      i + #m + j + k == #m + i + (j + k) *)
     1.7 -	    listof (Data.prove_conv [Data.norm_tac] sg 
     1.8 -		    (t, 
     1.9 -		     Data.mk_bal (newshape(n1,terms1'), 
    1.10 -				  newshape(n2,terms2'))))
    1.11 +	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    1.12 +		raise TERM("cancel_numerals", []) 
    1.13 +	    else
    1.14 +		listof (Data.prove_conv [Data.norm_tac] sg 
    1.15 +			(t, 
    1.16 +			 Data.mk_bal (newshape(n1,terms1'), 
    1.17 +				      newshape(n2,terms2'))))
    1.18    in
    1.19  
    1.20        if n2<=n1 then