src/Pure/display.ML
changeset 28840 049f0a8faa35
parent 28802 9ba30eeec7ce
child 29091 b81fe045e799
     1.1 --- a/src/Pure/display.ML	Tue Nov 18 18:25:42 2008 +0100
     1.2 +++ b/src/Pure/display.ML	Tue Nov 18 18:25:45 2008 +0100
     1.3 @@ -52,7 +52,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, arg) = Pretty.strs [name, Library.quote arg];
     1.8 +fun pretty_tag (name, arg) = Pretty.strs [name, 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