anchor.diff:                  else [], tm
               let vs, bod = collectvs tm
               ((if prec = 0 then pp_open_hvbox fmt 4
  -              else 
  -                  (pp_open_hvbox fmt 5
  -                   pp_print_string fmt "("))
  +              else (pp_open_hvbox fmt 5; pp_print_string fmt "("))
                pp_print_string fmt s
  -             (if isalnum s then pp_print_string fmt " "
  -              else ())
  +             (if isalnum s then pp_print_string fmt " " else ())
                do_list (fun (b, x) -> 
  -                     (if b then pp_print_string fmt "("
  -                      else ())
  -                     print_term 0 x
  -                     (if b then pp_print_string fmt ")"
  -                      else ())
  -                     pp_print_string fmt " ") (butlast vs)
  -             (if fst(last vs) then pp_print_string fmt "("
  -              else ())
  -             print_term 0 (snd(last vs))
  -             (if fst(last vs) then pp_print_string fmt ")"
  -              else ())
  +                (if b then pp_print_string fmt "(" else ())
  +                print_term fmt 0 x
  +                (if b then pp_print_string fmt ")" else ())
  +                pp_print_string fmt " ") (butlast vs)
  +             (if fst(last vs) then pp_print_string fmt "(" else ())
  +             print_term fmt 0 (snd(last vs))
  +             (if fst(last vs) then pp_print_string fmt ")" else ())
                pp_print_string fmt "."
  -             (if length vs = 1 then pp_print_string fmt " "
  -              else pp_print_space fmt ())
  -             print_term 0 bod
  -             (if prec = 0 then ()
  -              else pp_print_string fmt ")")
  +             (if length vs = 1 then pp_print_string fmt " " else pp_print_space fmt ())
  +             print_term fmt 0 bod
  +             (if prec = 0 then () else pp_print_string fmt ")")
                pp_close_box fmt ())
   
  -        and print_clauses cls = 
  -            match cls with
  -            | [c] ->
  -                print_clause c
  -            | c :: cs -> 
  -                print_clause c
  -                pp_print_break fmt 1 0
  -                pp_print_string fmt "| "
  -                print_clauses cs
  -            | _ ->
  -                failwith "print_clauses: Unhandled case."
  -
  -        and print_clause cl = 
  -            match cl with
  -            | [p; g; r] -> 
  -                print_term 1 p
  -                pp_print_string fmt " when "
  -                print_term 1 g
  -                pp_print_string fmt " -> "
  -                print_term 1 r
  -            | [p; r] -> 
  -                print_term 1 p
  -                pp_print_string fmt " -> "
  -                print_term 1 r
  -            | _ ->
  -                failwith "print_clause: Unhandled case."
  -
  -        fun tm ->
  -            try
  -                print_term 0 tm
  -            with Failure _ as ex ->
  -                (* NOTE :   We currently suppress certain exceptions which may be raised during
  -                            printing; however, we do log them for diagnostics purposes. *)
  -                logger.DebugException ("Suppressed exception in 'pp_print_term'.", ex)
  -
  -                // NOTE: suppress all exceptions in printing
  -                ()
  +    and print_clauses fmt cls = 
  +        match cls with
  +        | [c] ->
  +            print_clause fmt c
  +        | c :: cs -> 
  +            print_clause fmt c
  +            pp_print_break fmt 1 0
  +            pp_print_string fmt "| "
  +            print_clauses fmt cs
  +        | _ ->
  +            failwith "print_clauses: Unhandled case."
  +
  +    and print_clause fmt cl = 
  +        match cl with
  +        | [p; g; r] -> 
  +            print_term fmt 1 p
  +            pp_print_string fmt " when "
  +            print_term fmt 1 g
  +            pp_print_string fmt " -> "
  +            print_term fmt 1 r
  +        | [p; r] -> 
  +            print_term fmt 1 p
  +            pp_print_string fmt " -> "
  +            print_term fmt 1 r
  +        | _ ->
  +            failwith "print_clause: Unhandled case."
  +
  +
  +/// Prints a term (without quotes) to formatter.
  +let pp_print_term fmt tm =
  +    try
  +        PP_print_term.print_term fmt 0 tm
  +    with Failure _ as ex ->
  +        (* NOTE :   We currently suppress certain exceptions which may be raised during
  +                    printing; however, we do log them for diagnostics purposes. *)
  +        logger.DebugException ("Suppressed exception in 'pp_print_term'.", ex)
  +
  +        // NOTE: suppress all exceptions in printing
  +        ()
   
   (* ------------------------------------------------------------------------- *)
   (* Print term with quotes.                                                   *)
  
positive.code:                                                 if fst(Choice.get <| dest_const c) <> "SETSPEC" then fail()
                                                  else 
                                                      pp_print_string fmt "{"
                                                      print_term 0 fabs
                                                      pp_print_string fmt " | "
                                                      (let fvs = frees fabs
                                                       let bvs = frees babs
  
negative.code: (* ------------------------------------------------------------------------- *)
  
  /// Gets the name of a constant or variable.
  let name_of tm =
      match tm with
      | Var(x, _)
      | Const(x, _) -> x
      | _ -> ""
  
  (* ------------------------------------------------------------------------- *)
  