let rec mk_mult a b =
  try
    let op, xl = Arith.d_interp a in
      mk_mult_arith op xl b
  with
      Not_found -> 
        (try
           let op, yl = Arith.d_interp b in
             mk_mult_arith op yl a
         with
             Not_found -> P.make a b)
        
and mk_mult_arith op yl b =
  match op, yl with
    | Sym.Num(q), [] -> 
        Arith.mk_multq q b
    | Sym.Multq(q), [x] -> 
        Arith.mk_multq q (mk_mult x b)
    | Sym.Add, _ ->
        mk_mult_add b yl
    | _ ->
        assert false
        
and mk_mult_add a yl =
  Arith.mk_addl (Term.mapl (mk_mult a) yl)
    
and mk_multl al =
  List.fold_left mk_mult (Arith.mk_one()) al