changeset 14599 | c3177fffd31a |
parent 12785 | 27debaf2112d |
child 14981 | e73f8140af78 |
--- 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));