# HG changeset patch
# User wenzelm
# Date 1364990280 -7200
# Node ID 8e80ecfa3652f7f54cbaa86ed3b35d631ce3a0e4
# Parent  5dbe537087aaafb5577a831cde89f31f18c4eca7
tuned output -- less bullets;

diff -r 5dbe537087aa -r 8e80ecfa3652 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 03 10:15:43 2013 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 03 13:58:00 2013 +0200
@@ -1317,7 +1317,7 @@
       val prt_prems =
         (case Assumption.all_prems_of ctxt of
           [] => []
-        | prems => [Pretty.big_list "prems:" (map (Display.pretty_thm_item ctxt) prems)]);
+        | prems => [Pretty.big_list "prems:" [pretty_fact ctxt ("", prems)]]);
     in prt_structs @ prt_fixes @ prt_prems end;
 
 
diff -r 5dbe537087aa -r 8e80ecfa3652 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Apr 03 10:15:43 2013 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Apr 03 13:58:00 2013 +0200
@@ -113,9 +113,9 @@
 
 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);
+    [if s = "" then Pretty.str "this:"
+     else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"],
+     Proof_Context.pretty_fact ctxt ("", ths)];
 
 
 (* method_error *)