anchor.diff:      (* The rules are partitioned into association lists.                       *)
       (* ----------------------------------------------------------------------- *)
   
  -    let fol_of_hol_clauses = 
  -        let eqt (a1, (b1, c1)) (a2, (b2, c2)) = 
  +    let fol_of_hol_clauses =
  +        let eqt (a1, (b1, c1)) (a2, (b2, c2)) =
               ((a1 = a2) && (b1 = b2) && (equals_thm c1 c2))
   
           let mk_negated(p, a) = -p, a
   
  -        let rec mk_contraposes n th used unused sofar = 
  +        let rec mk_contraposes n th used unused sofar =
               match unused with
               | [] -> sofar
  -            | h :: t -> 
  +            | h :: t ->
                   let nw = (map mk_negated (used @ t), h), (n, th)
                   mk_contraposes (n + 1) th (used @ [h]) t (nw :: sofar)
   
  -        let fol_of_hol_clause th = 
  +        let fol_of_hol_clause th =
               choice {
                   let! th = th
                   let lconsts = freesl <| hyp th
  
positive.code:             let v =
                  try 
                      if !meson_prefine && pr > 0 then 
                          failwith "meson_expand"
                      else 
                          let arules = assoc pr ancestors |> Option.getOrFailWith "find"
                          Choice.result <| meson_expand_cont 0 arules newstate cont
                  with
                  | Cut as e -> 
                      Choice.nestedFailwith e "meson_expand"
                  | Failure _ -> 
                      try 
  
negative.code:     (* Test for equality under the pending instantiations.                     *)
      (* ----------------------------------------------------------------------- *)
  
      let rec fol_eq insts tm1 tm2 =
          tm1 == tm2 ||
          match tm1, tm2 with
          | Fnapp(f, fargs), Fnapp(g, gargs) ->
              f = g && forall2 (fol_eq insts) fargs gargs
          | _, Fvar(x) ->
              match rev_assoc x insts with
              | Some tm2' ->
                   fol_eq insts tm1 tm2'
              | None ->
                   istriv insts x tm1
                   |> Choice.fill false
  
          | Fvar(x), _ ->
              match rev_assoc x insts with
              | Some tm1' ->
                   fol_eq insts tm1' tm2
              | None ->
                   istriv insts x tm2
                   |> Choice.fill false
  
      let fol_atom_eq insts (p1, args1) (p2, args2) =
          p1 = p2 && forall2 (fol_eq insts) args1 args2
  
      (* ----------------------------------------------------------------------- *)
      (* Cacheing continuations. Very crude, but it works remarkably well.       *)
      (* ----------------------------------------------------------------------- *)
  
      let cacheconts f =
          let cacheconts_memory : ('a * ('b * 'c * 'd)) list ref = ref []
          fun (_, (insts, _, size) as input) ->
              if exists (fun (_, (insts', _, size')) -> insts = insts' && (size <= size' || !meson_depth)) !cacheconts_memory then
                  failwith "cacheconts"
              else 
                  cacheconts_memory := input :: !cacheconts_memory
                  f input
  
      (* ----------------------------------------------------------------------- *)
  