def split_instr(instr):
  """
  Given an instruction of the form "name arg1, arg2, ...",
  returns the pair ("name", "arg1, arg2, ...").

  If the instruction has no arguments, the second element of
  the pair is the empty string.
  """
  result = instr.split(None, 1)
  if len(result) == 1:
    return result[0], ""
  else:
    return result