src/Pure/display.ML
changeset 23657 2332c79f4dc8
parent 23634 55e579ef85aa
child 24665 e5bea50b9b89
     1.1 --- a/src/Pure/display.ML	Sun Jul 08 19:52:04 2007 +0200
     1.2 +++ b/src/Pure/display.ML	Sun Jul 08 19:52:05 2007 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
     1.5  val show_tags = ref false;      (*false: suppress tags*)
     1.6  
     1.7 -fun pretty_tag (name, args) = Pretty.strs (name :: map Library.quote args);
     1.8 +fun pretty_tag (name, arg) = Pretty.strs [name, Library.quote arg];
     1.9  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    1.10  
    1.11  fun pretty_flexpair pp (t, u) = Pretty.block