anchor.diff:  (* version to avoid a great deal of reuilding of terms.                      *)
   (* ------------------------------------------------------------------------- *)
   
  -let (ONCE_DEPTH_CONV: conv->conv),
  -    (DEPTH_CONV: conv->conv),
  -    (REDEPTH_CONV: conv->conv),
  -    (TOP_DEPTH_CONV: conv->conv),
  -    (TOP_SWEEP_CONV: conv->conv) =
  -  let rec THENQC conv1 conv2 tm =
  -    try let th1 = conv1 tm in
  -        try let th2 = conv2(rand(concl th1)) in TRANS th1 th2
  +let rec private THENQC conv1 conv2 tm =
  +    try
  +        let th1 = conv1 tm
  +        try
  +            let th2 = conv2(rand(concl th1))
  +            TRANS th1 th2
           with Failure _ -> th1
       with Failure _ -> conv2 tm
  -  and THENCQC conv1 conv2 tm =
  -    let th1 = conv1 tm in
  -    try let th2 = conv2(rand(concl th1)) in TRANS th1 th2
  +
  +and private THENCQC conv1 conv2 tm =
  +    let th1 = conv1 tm
  +    try
  +        let th2 = conv2(rand(concl th1))
  +        TRANS th1 th2
       with Failure _ -> th1
  -  and COMB_QCONV conv tm =
  -    let l,r = dest_comb tm in
  -    try let th1 = conv l in
  -        try let th2 = conv r in MK_COMB(th1,th2)
  -        with Failure _ -> AP_THM th1 r
  -    with Failure _ -> AP_TERM l (conv r) in
  -  let rec REPEATQC conv tm = THENCQC conv (REPEATQC conv) tm in
  -  let SUB_QCONV conv tm =
  +
  +and private COMB_QCONV conv tm =
  +    let l,r = dest_comb tm
  +    try
  +        let th1 = conv l
  +        try
  +            let th2 = conv r
  +            MK_COMB(th1,th2)
  +        with Failure _ ->
  +            AP_THM th1 r
  +    with Failure _ ->
  +        AP_TERM l (conv r)
  +
  +let rec private REPEATQC conv tm =
  +    THENCQC conv (REPEATQC conv) tm
  +
  +let private SUB_QCONV conv tm =
       if is_abs tm then ABS_CONV conv tm
  -    else COMB_QCONV conv tm in
  -  let rec ONCE_DEPTH_QCONV conv tm =
  -      (conv ORELSEC (SUB_QCONV (ONCE_DEPTH_QCONV conv))) tm
  -  and DEPTH_QCONV conv tm =
  +    else COMB_QCONV conv tm
  +
  +let rec private ONCE_DEPTH_QCONV conv tm =
  +      (ORELSEC conv (SUB_QCONV (ONCE_DEPTH_QCONV conv))) tm
  +
  +and private DEPTH_QCONV conv tm =
       THENQC (SUB_QCONV (DEPTH_QCONV conv))
              (REPEATQC conv) tm
  -  and REDEPTH_QCONV conv tm =
  +
  +and private REDEPTH_QCONV conv tm =
       THENQC (SUB_QCONV (REDEPTH_QCONV conv))
              (THENCQC conv (REDEPTH_QCONV conv)) tm
  -  and TOP_DEPTH_QCONV conv tm =
  +
  +and private TOP_DEPTH_QCONV conv tm =
       THENQC (REPEATQC conv)
              (THENCQC (SUB_QCONV (TOP_DEPTH_QCONV conv))
                       (THENCQC conv (TOP_DEPTH_QCONV conv))) tm
  -  and TOP_SWEEP_QCONV conv tm =
  +
  +and private TOP_SWEEP_QCONV conv tm =
       THENQC (REPEATQC conv)
  -           (SUB_QCONV (TOP_SWEEP_QCONV conv)) tm in
  -  (fun c -> TRY_CONV (ONCE_DEPTH_QCONV c)),
  -  (fun c -> TRY_CONV (DEPTH_QCONV c)),
  -  (fun c -> TRY_CONV (REDEPTH_QCONV c)),
  -  (fun c -> TRY_CONV (TOP_DEPTH_QCONV c)),
  -  (fun c -> TRY_CONV (TOP_SWEEP_QCONV c))
  +           (SUB_QCONV (TOP_SWEEP_QCONV conv)) tm
  +
  +let ONCE_DEPTH_CONV (c : conv) : conv =
  +    TRY_CONV (ONCE_DEPTH_QCONV c)
  +
  +let DEPTH_CONV (c : conv) : conv =
  +    TRY_CONV (DEPTH_QCONV c)
  +
  +let REDEPTH_CONV (c : conv) : conv =
  +    TRY_CONV (REDEPTH_QCONV c)
  +
  +let TOP_DEPTH_CONV (c : conv) : conv =
  +    TRY_CONV (TOP_DEPTH_QCONV c)
  +
  +let TOP_SWEEP_CONV (c : conv) : conv =
  +    TRY_CONV (TOP_SWEEP_QCONV c)
  +
   
   (* ------------------------------------------------------------------------- *)
   (* Apply at leaves of op-tree; NB any failures at leaves cause failure.      *)
  
positive.code:             let pat = subst (zip gvs lefts) tm
              let abs = list_mk_abs(gvs,pat)
              let th = rev_itlist
                        (fun y x -> CONV_RULE (RAND_CONV BETA_CONV THENC LAND_CONV BETA_CONV)
                                      (MK_COMB(x,y))) ths (REFL abs)
              if rand(concl th) = tm then REFL tm else th
      with Failure _ ->
  
negative.code:   match tm with
    | Comb(Comb(op',l),r) when op' = op ->
        let l,r = dest_binop op tm
        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
  
  