anchor.diff:                  let hlits = disjuncts tm
                   let! flits = Choice.List.map (fol_of_literal [] lconsts) hlits
                   let basics = mk_contraposes 0 (Choice.result th) [] flits []
  -                if forall (fun (p, _) -> p < 0) flits then 
  +                if forall (fun (p, _) -> p < 0) flits then
                       return ((map mk_negated flits, (1, [])), (-1, Choice.result th)) :: basics
  -                else 
  +                else
                       return basics
               }
   
  -        fun thms -> 
  +        fun thms ->
               let rawrules = itlist (union' eqt << Choice.get << fol_of_hol_clause) thms []
               let prs = setify(map (fst << snd << fst) rawrules)
               let prules = map (fun t -> t, filter ((=) t << fst << snd << fst) rawrules) prs
  
positive.code:                                 | _ -> false) 
                              equals_thm 
                              (mapfilter (Choice.toOption << Choice.map Choice.result << C INST_TYPE th) tyins)
                      if ths' = [] then 
                          warn true "No useful-looking instantiations of lemma"
                          return [th]
                      else 
  
negative.code:                                         else cont(lg' @ rg', ztup)))))
                  else 
                      match gl with
                      | g :: gs ->
                          expand_goal depth (g, tup)
                              (cacheconts
                                   (fun (g', stup) ->
                                      expand_goals depth (gs, stup) (cacheconts(fun (gs', ftup) -> cont(g' :: gs', ftup)))))
                          |> Choice.toOption
                      | _ -> None
          
          fun g maxdep maxinf cont ->
              expand_goal maxdep (g, ([], 2 * offinc, maxinf)) cont
  
      (* ----------------------------------------------------------------------- *)
      (* With iterative deepening of inferences or depth.                        *)
      (* ----------------------------------------------------------------------- *)
  
      let solve_goal rules incdepth min max incsize =
          let rec solve n g =
              if n > max then
                  Choice.failwith "solve_goal: Too deep"
              else
                  if !verbose then
                      if !meson_chatty then
                          Format.print_string ((string !inferences) + " inferences so far. " + "Searching with maximum size " + (string n) + ".")
                          Format.print_newline ()
                  
                      Format.print_string ((string !inferences) + "..")
                      Format.print_flush ()
                   
                  let gi =
                      if incdepth then
                          expand_goal rules g n 100000 Some
                      else
                          expand_goal rules g 100000 n Some
  
                  if !verbose then
                      if !meson_chatty then
                          Format.print_string ("Goal solved with " + (string !inferences) + " inferences.")
                          Format.print_newline ()
                  
                      Format.print_string ("solved at " + string !inferences)
                      Format.print_newline ()
  
                  // NOTE : We manually pattern-match on the value of 'gi' here; calling Choice.bindError
                  // to continue recursing would make this function non-tail-recursive.
                  match gi with
                  | Success _ as result ->
                      result
                  | Error _ ->
                      solve (n + incsize) g
  
          fun g ->
              solve min (g, [])
  
      (* ----------------------------------------------------------------------- *)
      (* Creation of tagged contrapositives from a HOL clause.                   *)
  