src/Pure/display.ML
changeset 14598 7009f59711e3
parent 14472 cba7c0a3ffb3
child 14644 3224082514f9
     1.1 --- a/src/Pure/display.ML	Fri Apr 16 18:44:39 2004 +0200
     1.2 +++ b/src/Pure/display.ML	Fri Apr 16 18:45:56 2004 +0200
     1.3 @@ -64,7 +64,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 quote args);
     1.8 +fun pretty_tag (name, args) = Pretty.strs (name :: map Library.quote args);
     1.9  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    1.10  
    1.11  fun pretty_flexpair pretty_term (t, u) = Pretty.block
    1.12 @@ -166,8 +166,8 @@
    1.13  fun pretty_name_space (kind, space) =
    1.14    let
    1.15      fun prt_entry (name, accs) = Pretty.block
    1.16 -      (Pretty.str (quote name ^ " =") :: Pretty.brk 1 ::
    1.17 -        Pretty.commas (map (Pretty.str o quote) accs));
    1.18 +      (Pretty.str (Library.quote name ^ " =") :: Pretty.brk 1 ::
    1.19 +        Pretty.commas (map (Pretty.quote o Pretty.str) accs));
    1.20    in
    1.21      Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space))
    1.22      |> Pretty.block