# HG changeset patch
# User wenzelm
# Date 912519995 -3600
# Node ID aa84c30c1f610cb746c929873dbbc720dc03f22b
# Parent  84fe61a08c1754f82796bae31d1a3fe29fe72640
show_tags flag;

diff -r 84fe61a08c17 -r aa84c30c1f61 src/Pure/attribute.ML
--- a/src/Pure/attribute.ML	Tue Dec 01 10:39:35 1998 +0100
+++ b/src/Pure/attribute.ML	Tue Dec 01 14:46:35 1998 +0100
@@ -10,6 +10,7 @@
   type tag
   type tthm
   type 'a attribute
+  val show_tags: bool ref
 end;
 
 signature ATTRIBUTE =
@@ -70,12 +71,14 @@
 
 (* display tagged theorems *)
 
+val show_tags = ref false;
+
 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)
-  | pretty_tthm (thm, tags) = Pretty.block
-      [Pretty.quote (Display.pretty_thm thm), Pretty.brk 1, pretty_tags tags];
+fun pretty_tthm (thm, tags) =
+  if null tags orelse not (! show_tags) then Pretty.quote (Display.pretty_thm thm)
+  else 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));