anchor.diff:          else
               THENC (RATOR_CONV(BETAS_CONV(n - 1))) (TRY_CONV BETA_CONV) tm
   
  -    let rec HO_BETAS bcs pat tm = 
  +    let rec HO_BETAS bcs pat tm =
           if is_var pat || is_const pat then
               Choice.fail ()
           else 
  
positive.code:             choice {
                  let! (sth, bod, pbod, lconsts, fvs) = v
                  let bvms = match_bvs tm pbod []
                  let abod = deep_alpha bvms bod
                  let ath = EQ_MP (ALPHA bod abod) sth
                  let! tm1 = partfn abod
                  let! insts = term_match lconsts tm1 tm
  
negative.code:             |> Choice.bindError (fun _ ->
                  Choice.result tm))
      
      deep_alpha
  
  (* ------------------------------------------------------------------------- *)
  (* Instantiate theorem by matching part of it to a term.                     *)
  