# HG changeset patch
# User wenzelm
# Date 1238077250 -3600
# Node ID 2e54e89bcce75ebd0a8ea703f0aa74122a85b26f
# Parent  a3adc9a96a161770fa7d1dcd61e8b3b3acee0bb2
pretty_rule/print_results: no thm status here -- it is potentially slow and mostly uninformative/confusing as long as proofs are still unfinished;

diff -r a3adc9a96a16 -r 2e54e89bcce7 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Thu Mar 26 15:18:50 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML	Thu Mar 26 15:20:50 2009 +0100
@@ -32,8 +32,10 @@
   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;
@@ -66,7 +68,7 @@
 
 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;
 
@@ -81,7 +83,7 @@
 
 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
 
@@ -92,7 +94,7 @@
   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 ")"])]));