src/Provers/Arith/cancel_numerals.ML
changeset 14387 e96d5c42c4b0
parent 13484 d8f5d3391766
child 15027 d23887300b96
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Sat Feb 14 02:06:12 2004 +0100
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Sun Feb 15 10:46:37 2004 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4  signature CANCEL_NUMERALS_DATA =
     1.5  sig
     1.6    (*abstract syntax*)
     1.7 -  val mk_sum: term list -> term
     1.8 +  val mk_sum: typ -> term list -> term
     1.9    val dest_sum: term -> term list
    1.10    val mk_bal: term * term -> term
    1.11    val dest_bal: term -> term * term
    1.12 @@ -78,7 +78,8 @@
    1.13        val u = find_common (terms1,terms2)
    1.14        val (n1, terms1') = Data.find_first_coeff u terms1
    1.15        and (n2, terms2') = Data.find_first_coeff u terms2
    1.16 -      fun newshape (i,terms) = Data.mk_sum (Data.mk_coeff(i,u)::terms)
    1.17 +      and T = Term.fastype_of u
    1.18 +      fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms)
    1.19        val reshape =  (*Move i*u to the front and put j*u into standard form
    1.20  		       i + #m + j + k == #m + i + (j + k) *)
    1.21  	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    1.22 @@ -94,12 +95,12 @@
    1.23  	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
    1.24  		Data.numeral_simp_tac] sg hyps xs
    1.25  	       (t', Data.mk_bal (newshape(n1-n2,terms1'), 
    1.26 -				 Data.mk_sum terms2'))
    1.27 +				 Data.mk_sum T terms2'))
    1.28  	else
    1.29  	    Data.prove_conv 
    1.30  	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
    1.31  		Data.numeral_simp_tac] sg hyps xs
    1.32 -	       (t', Data.mk_bal (Data.mk_sum terms1', 
    1.33 +	       (t', Data.mk_bal (Data.mk_sum T terms1', 
    1.34  				 newshape(n2-n1,terms2'))))
    1.35    end
    1.36    handle TERM _ => None