| changeset 62819 | d3ff367a16a0 |
| parent 62663 | bea354f6ff21 |
| child 64556 | 851ae0e7b09c |
--- a/src/Pure/Syntax/ast.ML Sat Apr 02 20:33:34 2016 +0200 +++ b/src/Pure/Syntax/ast.ML Sat Apr 02 21:10:07 2016 +0200 @@ -66,7 +66,7 @@ fun pretty_rule (lhs, rhs) = Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs]; -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_ast); +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_ast); (* strip_positions *)