src/Pure/Isar/proof_display.ML

   val pretty_full_theory: bool -> theory -> Pretty.T
   val print_theory: theory -> unit
   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 method_error: string -> Position.T ->
     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
   val print_results: Markup.T -> bool -> Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
   val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit

 fun string_of_goal ctxt goal =
   Pretty.string_of (Pretty.chunks
     [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]);
 
 
+(* goal facts *)
+
+fun pretty_goal_facts ctxt s ths =
+  (Pretty.block o Pretty.fbreaks)
+    ((if s = "" then Pretty.str "this:"
+      else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) ::
+      map (Display.pretty_thm_item ctxt) ths);
+
+
 (* method_error *)
 
 fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
   let
     val pr_header =
       "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
       "proof method" ^ Position.here pos ^ ":\n";
     val pr_facts =
       if null facts then ""
-      else
-        (Pretty.string_of o Pretty.block o Pretty.fbreaks)
-          (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] ::
-            map (Display.pretty_thm ctxt) facts) ^ "\n";
+      else Pretty.string_of (pretty_goal_facts ctxt "using" facts) ^ "\n";
     val pr_goal = string_of_goal ctxt goal;
   in pr_header ^ pr_facts ^ pr_goal end);
 
 
 (* results *)