src/Pure/Isar/proof_display.ML

  (if ! ProofContext.debug then
     Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
   else Pretty.str "<context>");
 
 fun pp_thm th =
-  let val thy = Thm.theory_of_thm th
-  in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
+  let
+    val thy = Thm.theory_of_thm th;
+    val flags = {quote = true, show_hyps = false, show_status = true};
+  in Display.pretty_thm_aux (Syntax.pp_global thy) flags [] th end;
 
 val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
 val pp_term = Pretty.quote oo Syntax.pretty_term_global;
 
 fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);

 
 (* refinement rule *)
 
 fun pretty_rule ctxt s thm =
   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
-    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
+    Pretty.fbrk, ProofContext.pretty_thm_aux ctxt false thm];
 
 val string_of_rule = Pretty.string_of ooo pretty_rule;
 
 
 (* results *)

   | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
       Pretty.str (Long_Name.base_name name), Pretty.str ":"];
 
 fun pretty_facts ctxt =
   flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
-    map (single o ProofContext.pretty_fact ctxt);
+    map (single o ProofContext.pretty_fact_aux ctxt false);
 
 in
 
 fun print_results do_print ctxt ((kind, name), facts) =
   if not do_print orelse kind = "" orelse kind = Thm.internalK then ()
   else if name = "" then
     Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   else Pretty.writeln
     (case facts of
       [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
-        ProofContext.pretty_fact ctxt fact])
+        ProofContext.pretty_fact_aux ctxt false fact])
     | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
         Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
 
 end;