| changeset 62819 | d3ff367a16a0 |
| parent 62663 | bea354f6ff21 |
| child 62891 | 7a11ea5c9626 |
--- a/src/Pure/Concurrent/synchronized.ML Sat Apr 02 20:33:34 2016 +0200 +++ b/src/Pure/Concurrent/synchronized.ML Sat Apr 02 21:10:07 2016 +0200 @@ -69,6 +69,6 @@ (* toplevel pretty printing *) -val _ = PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => pretty (value var, depth)); +val _ = ML_system_pp (fn depth => fn pretty => fn var => pretty (value var, depth)); end;