# HG changeset patch
# User wenzelm
# Date 906717791 -7200
# Node ID 95e8692fda23de0c0dc03b2ad71c3b4a819797de
# Parent  64a8495201d1cf084ac3561bd663f9fc241d1df1
tuned pretty_tag;
tag attribute: append;

diff -r 64a8495201d1 -r 95e8692fda23 src/Pure/attribute.ML
--- a/src/Pure/attribute.ML	Fri Sep 25 12:01:47 1998 +0200
+++ b/src/Pure/attribute.ML	Fri Sep 25 12:03:11 1998 +0200
@@ -75,10 +75,7 @@
 
 (* display tagged theorems *)
 
-fun pretty_tag (name, []) = Pretty.str name
-  | pretty_tag (name, args) = Pretty.block
-      [Pretty.str name, Pretty.list "(" ")" (map Pretty.str args)];
-
+fun pretty_tag (name, args) = Pretty.strs (name :: args);
 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
 
 fun pretty_tthm (thm, []) = Pretty.quote (Display.pretty_thm thm)
@@ -88,7 +85,7 @@
 
 (* basic attributes *)
 
-fun tag tg (x, (thm, tags)) = (x, (thm, tg ins tags));
+fun tag tg (x, (thm, tags)) = (x, (thm, if tg mem tags then tags else tags @ [tg]));
 fun untag tg (x, (thm, tags)) = (x, (thm, tags \ tg));
 
 val lemma = ("lemma", []);