anchor.diff:      let rec PCONV xs pat conv = 
           if mem pat xs then conv
           elif not(exists (fun x -> free_in x pat) xs) then ALL_CONV
  -        elif is_comb pat then COMB2_CONV (PCONV xs (Choice.get <| rator pat) conv) (PCONV xs (Choice.get <| rand pat) conv)
  -        else ABS_CONV(PCONV xs (Choice.get <| body pat) conv)
  +        elif is_comb pat then
  +            let rat = rator pat
  +            let ran = rand pat
  +            fun tm -> 
  +                (rat, ran) 
  +                ||> Choice.bind2 (fun rat ran -> COMB2_CONV (PCONV xs rat conv) (PCONV xs ran conv) tm)
  +        else
  +            let tm' = body pat 
  +            fun tm -> tm' |> Choice.bind (fun tm' -> ABS_CONV(PCONV xs tm' conv) tm)
       fun pat -> 
           let xs, pbod = strip_abs pat
           PCONV xs pbod
  
positive.code: 
  /// Beta-reduces all the beta-redexes in the conclusion of a theorem.
  let BETA_RULE = CONV_RULE(REDEPTH_CONV BETA_CONV)
  /// Reverses the first equation(s) encountered in a top-down search.
  let GSYM = CONV_RULE(ONCE_DEPTH_CONV SYM_CONV)
  /// Makes simple term substitutions in a theorem using a given list of theorems.
  let SUBS ths = CONV_RULE(SUBS_CONV ths)
  
  
negative.code: let rec DEPTH_BINOP_CONV op conv tm = 
      match tm with
      | Comb(Comb(op', l), r) when op' = op -> 
          dest_binop op tm
          |> Choice.bind (fun (l, r) ->
              let lth = DEPTH_BINOP_CONV op conv l
              let rth = DEPTH_BINOP_CONV op conv r
              MK_COMB(AP_TERM op' lth, rth))
      | _ -> conv tm
  
  (* ------------------------------------------------------------------------- *)
  