tuned signature;

--- a/src/Pure/Isar/proof.ML	Mon Sep 05 13:32:09 2022 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Sep 05 17:53:45 2022 +0200
@@ -369,9 +369,6 @@
 
 local
 
-fun pretty_facts _ _ NONE = []
-  | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths];
-
 fun pretty_sep prts [] = prts
   | pretty_sep [] prts = prts
   | pretty_sep prts1 prts2 = prts1 @ [Pretty.str ""] @ prts2;
@@ -383,10 +380,11 @@
     val {context = ctxt, facts, mode, goal = _} = top state;
     val verbose = Config.get ctxt Proof_Context.verbose;
 
+    val prt_facts = Proof_Display.pretty_goal_facts ctxt;
+
     fun prt_goal (SOME (_, {statement = _, using, goal, before_qed = _, after_qed = _})) =
           pretty_sep
-            (pretty_facts ctxt "using"
-              (if mode <> Backward orelse null using then NONE else SOME using))
+            (prt_facts "using" (if mode <> Backward orelse null using then NONE else SOME using))
             ([Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal)
       | prt_goal NONE = [];
 
@@ -401,8 +399,8 @@
       [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @
     (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
     (if verbose orelse mode = Forward then
-       pretty_sep (pretty_facts ctxt "" (Option.map #1 facts)) (prt_goal (try find_goal state))
-     else if mode = Chain then pretty_facts ctxt "picking" (Option.map #1 facts)
+       pretty_sep (prt_facts "" (Option.map #1 facts)) (prt_goal (try find_goal state))
+     else if mode = Chain then prt_facts "picking" (Option.map #1 facts)
      else prt_goal (try find_goal state))
   end;
 

--- a/src/Pure/Isar/proof_display.ML	Mon Sep 05 13:32:09 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML	Mon Sep 05 17:53:45 2022 +0200
@@ -19,7 +19,7 @@
   val string_of_rule: Proof.context -> string -> thm -> string
   val pretty_goal_header: thm -> Pretty.T
   val string_of_goal: Proof.context -> thm -> string
-  val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
+  val pretty_goal_facts: Proof.context -> string -> thm list option -> Pretty.T list
   val method_error: string -> Position.T ->
     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
   val show_results: bool Config.T
@@ -239,11 +239,12 @@
 
 (* goal facts *)
 
-fun pretty_goal_facts ctxt s ths =
-  (Pretty.block o Pretty.fbreaks)
-    [if s = "" then Pretty.str "this:"
-     else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
-     Proof_Context.pretty_fact ctxt ("", ths)];
+fun pretty_goal_facts _ _ NONE = []
+  | pretty_goal_facts ctxt s (SOME ths) =
+      (single o Pretty.block o Pretty.fbreaks)
+        [if s = "" then Pretty.str "this:"
+         else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
+         Proof_Context.pretty_fact ctxt ("", ths)];
 
 
 (* method_error *)
@@ -255,7 +256,7 @@
       "proof method" ^ Position.here pos ^ ":\n";
     val pr_facts =
       if null facts then ""
-      else Pretty.string_of (pretty_goal_facts ctxt "using" facts) ^ "\n";
+      else Pretty.string_of (Pretty.chunks (pretty_goal_facts ctxt "using" (SOME facts))) ^ "\n";
     val pr_goal = string_of_goal ctxt goal;
   in pr_header ^ pr_facts ^ pr_goal end);