fun typecheck_general lmterm context lunify
    : (substitution * TTerm) option =
        SOME([], INT)

functor TYPECHECK(U:UNIFIER) = struct
  fun typecheck lmterm context : TTerm option =
      case typecheck_general lmterm context U.lunify of
          NONE => NONE
        | SOME result => SOME (#2 result)
end