override def unifyCB2(t:Term, ctx:CallContext):ComputationBounds[Boolean]=
    {
     if (ctx.checkStackOverflow) {
       CallCC(ctx)(Call{ (ctx:CallContext) => unifyCB2(t,ctx) });
     } else {
       if (t.isFunctional) {
         if (t.funName == name) {
            return unifySeqCB2(funArgs,t.funArgs,ctx.withCall);
         } else {
            Done(false);
         }
       } else {
          Done(false);
       }
     }
  }



def unifySeqCB2(x:Seq[Term],y:Seq[Term],ctx:CallContext):
                                             ComputationBounds[Boolean]=
  {
    if (x.isEmpty) {
       Done(y.isEmpty)
    } else {
       if (ctx.checkStackOverflow) {
         CallCC(ctx)(Call{ (ctx) => unifySeqCB2(x,y,ctx) });
       } else {
         x.head.onUnifyCB2(y.head,ctx.withCall) {
          (r:Boolean, ctx:CallContext) =>
             if (!r) {
               Done(false)
             } else {
               if (x.isEmpty) {
                  Done(y.isEmpty);
               }else{
                  unifySeqCB2(x.tail,y.tail,ctx.withCall)
               }
             }
         }
       }
    }
 }