anchor.diff:  
   let AP_TERM tm th =
     try MK_COMB(REFL tm,th)
  -  with Failure _ -> failwith "AP_TERM";;
  +  with Failure _ -> failwith "AP_TERM"
   
   let AP_THM th tm =
     try MK_COMB(th,REFL tm)
  -  with Failure _ -> failwith "AP_THM";;
  +  with Failure _ -> failwith "AP_THM"
   
   let SYM th =
  -  let tm = concl th in
  -  let l,r = dest_eq tm in
  -  let lth = REFL l in
  -  EQ_MP (MK_COMB(AP_TERM (rator (rator tm)) th,lth)) lth;;
  +  let tm = concl th
  +  let l,r = dest_eq tm
  +  let lth = REFL l
  +  EQ_MP (MK_COMB(AP_TERM (rator (rator tm)) th,lth)) lth
   
   let ALPHA tm1 tm2 =
     try TRANS (REFL tm1) (REFL tm2)
  -  with Failure _ -> failwith "ALPHA";;
  +  with Failure _ -> failwith "ALPHA"
   
   let ALPHA_CONV v tm =
  -  let res = alpha v tm in
  -  ALPHA tm res;;
  +  let res = alpha v tm
  +  ALPHA tm res
   
   let GEN_ALPHA_CONV v tm =
     if is_abs tm then ALPHA_CONV v tm else
  -  let b,abs = dest_comb tm in
  -  AP_TERM b (ALPHA_CONV v abs);;
  +  let b,abs = dest_comb tm
  +  AP_TERM b (ALPHA_CONV v abs)
   
   let MK_BINOP op (lth,rth) =
  -  MK_COMB(AP_TERM op lth,rth);;
  +  MK_COMB(AP_TERM op lth,rth)
   
   (* ------------------------------------------------------------------------- *)
   (* Terminal conversion combinators.                                          *)
   (* ------------------------------------------------------------------------- *)
   
  -let (NO_CONV:conv) = fun tm -> failwith "NO_CONV";;
  -
  -let (ALL_CONV:conv) = REFL;;
  +let (NO_CONV:conv) = fun tm -> failwith "NO_CONV"
  +
  +let (ALL_CONV:conv) = REFL
   
   (* ------------------------------------------------------------------------- *)
   (* Combinators for sequencing, trying, repeating etc. conversions.           *)
  
positive.code:       [] -> cnv
      | "l"::t -> RATOR_CONV (path_conv t cnv)
      | "r"::t -> RAND_CONV (path_conv t cnv)
      | _::t -> ABS_CONV (path_conv t cnv) in
    fun s cnv -> path_conv (explode s) cnv;;
  
  (* ------------------------------------------------------------------------- *)
  (* Follow a pattern                                                          *)
  
negative.code:   (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))
  
  (* ------------------------------------------------------------------------- *)
  (* Apply at leaves of op-tree; NB any failures at leaves cause failure.      *)
  