let matching3  = 
  let rec 
    match_rec s = function 
        (Var(x), t) -> add_subst2 s (x,t)
      | (Operation(op_f,sons_f),Operation(op_t,sons_t)) ->
          if op_f = op_t then 
            try 
              (List.fold_left match_rec s 
                 (List.combine sons_f sons_t))
            with 
                (Invalid_argument "List.combine") -> 
                  raise (Match_exc("the operator "^op_f^
                                   " has different numbers of arguments"))
          else raise (Match_exc "operator incompatibility")
      | _ -> raise (Match_exc "operator incompatibility")
  in
    match_rec []