# HG changeset patch
# User berghofe
# Date 1082134020 -7200
# Node ID c3177fffd31a8441a58c32c83d5fe17dc3b20a7d
# Parent  7009f59711e367c6fd04b3748d10fb1982fdf77b
Replaced quote by Pretty.quote.

diff -r 7009f59711e3 -r c3177fffd31a src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Fri Apr 16 18:45:56 2004 +0200
+++ b/src/Pure/Syntax/ast.ML	Fri Apr 16 18:47:00 2004 +0200
@@ -81,7 +81,7 @@
 
 (* pretty_ast *)
 
-fun pretty_ast (Constant a) = Pretty.str (quote a)
+fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
   | pretty_ast (Variable x) = Pretty.str x
   | pretty_ast (Appl asts) =
       Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));