src/ZF/arith_data.ML
changeset 24630 351a308ab58d
parent 20342 4392003fcbfa
child 24893 b8ef7afe3a6b
     1.1 --- a/src/ZF/arith_data.ML	Tue Sep 18 11:06:22 2007 +0200
     1.2 +++ b/src/ZF/arith_data.ML	Tue Sep 18 16:08:00 2007 +0200
     1.3 @@ -100,13 +100,13 @@
     1.4        handle TERM _ => [t];
     1.5  
     1.6  (*Dummy version: the only arguments are 0 and 1*)
     1.7 -fun mk_coeff (0: IntInf.int, t) = zero
     1.8 +fun mk_coeff (0, t) = zero
     1.9    | mk_coeff (1, t) = t
    1.10    | mk_coeff _       = raise TERM("mk_coeff", []);
    1.11  
    1.12  (*Dummy version: the "coefficient" is always 1.
    1.13    In the result, the factors are sorted terms*)
    1.14 -fun dest_coeff t = (1 : IntInf.int, mk_prod (sort Term.term_ord (dest_prod t)));
    1.15 +fun dest_coeff t = (1, mk_prod (sort Term.term_ord (dest_prod t)));
    1.16  
    1.17  (*Find first coefficient-term THAT MATCHES u*)
    1.18  fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])