src/Pure/Syntax/syntax.ML

   val pretty_typ_global: theory -> typ -> Pretty.T
   val pretty_sort_global: theory -> sort -> Pretty.T
   val string_of_term_global: theory -> term -> string
   val string_of_typ_global: theory -> typ -> string
   val string_of_sort_global: theory -> sort -> string
+  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   type syntax
   val eq_syntax: syntax * syntax -> bool
   val force_syntax: syntax -> unit
   datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int}
   val get_approx: syntax -> string -> approx option

 val string_of_term_global = string_of_term o init_pretty_global;
 val string_of_typ_global = string_of_typ o init_pretty_global;
 val string_of_sort_global = string_of_sort o init_pretty_global;
 
 
+(* derived operations *)
+
+fun pretty_flexpair ctxt (t, u) = Pretty.block
+  [pretty_term ctxt t, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, pretty_term ctxt u];
+
+
 
 (** tables of translation functions **)
 
 (* parse (ast) translations *)
 

 
 
 open Lexicon.Syntax;
 
 end;
-