public static Proposition finishCreatingFunctionProposition(Proposition proposition) {
    { int argcount = proposition.arguments.length();
      NamedDescription description = Logic.getDescription(proposition.operator);
      Surrogate type = null;
      Skolem skolem = null;

      if (description != null) {
        type = Logic.unwrapWrappedType(((Surrogate)(description.ioVariableTypes.last())));
      }
      { Object old$Context$000 = Stella.$CONTEXT$.get();
        Object old$Module$000 = Stella.$MODULE$.get();

        try {
          Native.setSpecial(Stella.$CONTEXT$, proposition.homeContext);
          Native.setSpecial(Stella.$MODULE$, ((Context)(Stella.$CONTEXT$.get())).baseModule);
          skolem = Logic.createVariableOrSkolem(type, null);

        } finally {
          Stella.$MODULE$.set(old$Module$000);
          Stella.$CONTEXT$.set(old$Context$000);
        }
      }
      (proposition.arguments.theArray)[(argcount - 1)] = skolem;
      skolem.definingProposition = proposition;
      if (type != null) {
        Skolem.updateSkolemType(skolem, type);
      }
      if (proposition.operator == Logic.SGT_PL_KERNEL_KB_VALUE) {
        proposition = Proposition.normalizeValueFunction(proposition);
      }
      else {
        Proposition.normalizeFunctionProposition(proposition);
      }
      Proposition.verifyArgumentTypesAndCount(proposition);
      if (Stella_Object.isaP(proposition.operator, Logic.SGT_STELLA_SURROGATE)) {
        Proposition.fastenDownOneProposition(proposition, true);
        Proposition.helpFastenDownPropositions(proposition, false);
      }
      return (proposition);
    }
  }