tuned output -- less bullets;

--- 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;
 
 

--- 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 *)