# HG changeset patch
# User wenzelm
# Date 1662634361 -7200
# Node ID 1202e29798a4babc64d72654800ed08bf8104e50
# Parent  730638d4e37a85664d7b1fa1f0d6c7ee224a4766
tuned signature;

diff -r 730638d4e37a -r 1202e29798a4 src/Pure/Syntax/syntax.ML
--- 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];
 
 
diff -r 730638d4e37a -r 1202e29798a4 src/Pure/goal_display.ML
--- 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;
diff -r 730638d4e37a -r 1202e29798a4 src/Pure/more_thm.ML
--- 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 =
diff -r 730638d4e37a -r 1202e29798a4 src/Pure/proofterm.ML
--- 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