# HG changeset patch
# User wenzelm
# Date 911307872 -3600
# Node ID a8e1ca1b2ec6a760701e96c12c1fa1657f36a7b9
# Parent  258021e279807af88da00d4deff87fff6d665d0b
added pretty_tthms, print_tthms;
tuned apply(s);

diff -r 258021e27980 -r a8e1ca1b2ec6 src/Pure/attribute.ML
--- a/src/Pure/attribute.ML	Tue Nov 17 10:29:28 1998 +0100
+++ b/src/Pure/attribute.ML	Tue Nov 17 14:04:32 1998 +0100
@@ -26,7 +26,9 @@
   val apply: ('a * tthm) * 'a attribute list -> ('a * tthm)
   val applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list)
   val pretty_tthm: tthm -> Pretty.T
+  val pretty_tthms: tthm list -> Pretty.T
   val print_tthm: tthm -> unit
+  val print_tthms: tthm list -> unit
   val tag: tag -> 'a attribute
   val untag: tag -> 'a attribute
   val lemma: tag
@@ -62,15 +64,8 @@
 
 (* apply attributes *)
 
-fun apply (x_th, []) = x_th
-  | apply (x_th, f :: fs) = apply (f x_th, fs);
-
-fun applys ((x, []), _) = (x, [])
-  | applys ((x, th :: ths), atts) =
-      let
-        val (x', th') = apply ((x, th), atts);
-        val (x'', ths') = applys ((x', ths), atts);
-      in (x'', th' :: ths') end;
+fun apply (x_th, atts) = Library.apply atts x_th;
+fun applys (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
 
 
 (* display tagged theorems *)
@@ -82,7 +77,11 @@
   | pretty_tthm (thm, tags) = Pretty.block
       [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
 
+fun pretty_tthms [th] = pretty_tthm th
+  | pretty_tthms ths = Pretty.block (Pretty.fbreaks (map pretty_tthm ths));
+
 val print_tthm = Pretty.writeln o pretty_tthm;
+val print_tthms = Pretty.writeln o pretty_tthms;
 
 
 (* basic attributes *)