--- a/src/Pure/more_thm.ML Sun Feb 25 19:30:55 2018 +0100
+++ b/src/Pure/more_thm.ML Sun Feb 25 19:43:38 2018 +0100
@@ -705,7 +705,7 @@
val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
fun pretty_flexpair ctxt (t, u) = Pretty.block
- [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
+ [Syntax.pretty_term ctxt t, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, Syntax.pretty_term ctxt u];
fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
let