--- a/src/Pure/display.ML Fri Apr 16 18:44:39 2004 +0200
+++ b/src/Pure/display.ML Fri Apr 16 18:45:56 2004 +0200
@@ -64,7 +64,7 @@
val show_hyps = ref false; (*false: print meta-hypotheses as dots*)
val show_tags = ref false; (*false: suppress tags*)
-fun pretty_tag (name, args) = Pretty.strs (name :: map quote args);
+fun pretty_tag (name, args) = Pretty.strs (name :: map Library.quote args);
val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
fun pretty_flexpair pretty_term (t, u) = Pretty.block
@@ -166,8 +166,8 @@
fun pretty_name_space (kind, space) =
let
fun prt_entry (name, accs) = Pretty.block
- (Pretty.str (quote name ^ " =") :: Pretty.brk 1 ::
- Pretty.commas (map (Pretty.str o quote) accs));
+ (Pretty.str (Library.quote name ^ " =") :: Pretty.brk 1 ::
+ Pretty.commas (map (Pretty.quote o Pretty.str) accs));
in
Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space))
|> Pretty.block