--- 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;
-