public static Cons updateTopLevelProposition(Stella_Object tree, Keyword updatemode) {
    if ((updatemode == Logic.KWD_ASSERT_FALSE) ||
        ((updatemode == Logic.KWD_PRESUME_FALSE) ||
         (updatemode == Logic.KWD_RETRACT_FALSE))) {
      tree = Cons.list$(Cons.cons(Logic.SYM_STELLA_NOT, Cons.cons(tree, Cons.cons(Stella.NIL, Stella.NIL))));
      updatemode = Logic.invertUpdateMode(updatemode);
    }
    else {
    }
    if (updatemode == Logic.KWD_ASSERT_TRUE) {
      { Object old$Automaticinstancetable$000 = Logic.$AUTOMATICINSTANCETABLE$.get();

        try {
          Native.setSpecial(Logic.$AUTOMATICINSTANCETABLE$, null);
          return (Proposition.helpUpdateTopLevelProposition(Logic.buildTopLevelProposition(tree, true), updatemode));

        } finally {
          Logic.$AUTOMATICINSTANCETABLE$.set(old$Automaticinstancetable$000);
        }
      }
    }
    else {
      return (Proposition.helpUpdateTopLevelProposition(Logic.buildTopLevelProposition(tree, false), updatemode));
    }
  }