# HG changeset patch
# User wenzelm
# Date 1364642019 -3600
# Node ID 9100c8e66b697beaef2e09192e7683c7a8a98ab8
# Parent  a6b1f63ae1cb19c6fd1eaab4cc04e422f8bb7322
item markup for Proof_Context.pretty_fact;
tuned signature;

diff -r a6b1f63ae1cb -r 9100c8e66b69 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 30 11:43:17 2013 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 30 12:13:39 2013 +0100
@@ -394,7 +394,7 @@
   |> Pretty.chunks2 |> Pretty.string_of;
 
 fun string_of_thms ctxt args =
-  Pretty.string_of (Display.pretty_thms ctxt (Attrib.eval_thms ctxt args));
+  Pretty.string_of (Proof_Context.pretty_fact ctxt ("", Attrib.eval_thms ctxt args));
 
 fun string_of_prfs full state arg =
   Pretty.string_of
diff -r a6b1f63ae1cb -r 9100c8e66b69 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 30 11:43:17 2013 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 30 12:13:39 2013 +0100
@@ -342,11 +342,16 @@
 fun pretty_fact_name ctxt a =
   Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"];
 
-fun pretty_fact ctxt ("", ths) = Display.pretty_thms ctxt ths
-  | pretty_fact ctxt (a, [th]) = Pretty.block
-      [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm ctxt th]
-  | pretty_fact ctxt (a, ths) = Pretty.block
-      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm ctxt) ths));
+fun pretty_fact ctxt =
+  let
+    val pretty_thm = Display.pretty_thm ctxt;
+    val pretty_thms = map (Pretty.item o single o pretty_thm);
+  in
+    fn ("", [th]) => pretty_thm th
+     | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths))
+     | (a, [th]) => Pretty.block [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm th]
+     | (a, ths) => Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: pretty_thms ths))
+  end;
 
 
 
diff -r a6b1f63ae1cb -r 9100c8e66b69 src/Pure/display.ML
--- a/src/Pure/display.ML	Sat Mar 30 11:43:17 2013 +0100
+++ b/src/Pure/display.ML	Sat Mar 30 12:13:39 2013 +0100
@@ -25,7 +25,6 @@
   val string_of_thm: Proof.context -> thm -> string
   val string_of_thm_global: theory -> thm -> string
   val string_of_thm_without_context: thm -> string
-  val pretty_thms: Proof.context -> thm list -> Pretty.T
   val pretty_full_theory: bool -> theory -> Pretty.T list
 end;
 
@@ -91,12 +90,6 @@
 val string_of_thm_without_context = Pretty.string_of o pretty_thm_without_context;
 
 
-(* multiple theorems *)
-
-fun pretty_thms ctxt [th] = pretty_thm ctxt th
-  | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
-
-
 
 (** print theory **)