public static void verifyEvaluableOperator(Stella_Object operator, Keyword kind) {
    if (Surrogate.subtypeOfP(Stella_Object.safePrimaryType(operator), Logic.SGT_LOGIC_PATTERN_VARIABLE)) {
      { PatternVariable operator000 = ((PatternVariable)(operator));

        if (kind == Logic.KWD_PREDICATE) {
          operator000.skolemType = Logic.SGT_PL_KERNEL_KB_RELATION;
        }
        else if (kind == Logic.KWD_FUNCTION) {
          operator000.skolemType = Logic.SGT_PL_KERNEL_KB_FUNCTION;
        }
        else {
          { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

            stream000.nativeStream.print("`" + kind + "' is not a valid case option");
            throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
          }
        }
      }
    }
    else {
    }
  }