diff -r 6410166400ea -r a21a96eda033 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -70,6 +70,7 @@
   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
@@ -344,6 +345,12 @@
 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 **)
 
@@ -678,4 +685,3 @@
 open Lexicon.Syntax;
 
 end;
-