--- a/src/Pure/Syntax/syntax.ML Thu Sep 08 12:43:40 2022 +0200
+++ b/src/Pure/Syntax/syntax.ML Thu Sep 08 12:52:41 2022 +0200
@@ -70,7 +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
+ val pretty_flexpair: Proof.context -> term * term -> Pretty.T list
type syntax
val eq_syntax: syntax * syntax -> bool
val force_syntax: syntax -> unit
@@ -346,7 +346,7 @@
(* derived operations *)
-fun pretty_flexpair ctxt (t, u) = Pretty.block
+fun pretty_flexpair ctxt (t, u) =
[pretty_term ctxt t, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, pretty_term ctxt u];
--- a/src/Pure/goal_display.ML Thu Sep 08 12:43:40 2022 +0200
+++ b/src/Pure/goal_display.ML Thu Sep 08 12:52:41 2022 +0200
@@ -93,7 +93,7 @@
Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
- val pretty_ffpairs = pretty_list "flex-flex pairs:" (Syntax.pretty_flexpair ctxt);
+ val pretty_ffpairs = pretty_list "flex-flex pairs:" (Pretty.block o Syntax.pretty_flexpair ctxt);
val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
--- a/src/Pure/more_thm.ML Thu Sep 08 12:43:40 2022 +0200
+++ b/src/Pure/more_thm.ML Thu Sep 08 12:52:41 2022 +0200
@@ -731,7 +731,7 @@
if hlen = 0 then []
else if show_hyps orelse show_hyps' then
[Pretty.brk 2, Pretty.list "[" "]"
- (map (q o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
+ (map (q o Pretty.block o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
map (Syntax.pretty_sort ctxt) extra_shyps)]
else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
val tsymbs =
--- a/src/Pure/proofterm.ML Thu Sep 08 12:43:40 2022 +0200
+++ b/src/Pure/proofterm.ML Thu Sep 08 12:52:41 2022 +0200
@@ -1860,8 +1860,8 @@
fun search _ [] =
error ("Unsolvable constraints:\n" ^
Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
- Syntax.pretty_flexpair (Syntax.init_pretty_global thy)
- (apply2 (Envir.norm_term bigenv) p)) cs)))
+ Pretty.block (Syntax.pretty_flexpair (Syntax.init_pretty_global thy)
+ (apply2 (Envir.norm_term bigenv) p))) cs)))
| search env ((u, p as (t1, t2), vs)::ps) =
if u then
let