| changeset 62819 | d3ff367a16a0 |
| parent 62663 | bea354f6ff21 |
| child 62891 | 7a11ea5c9626 |
| 62818:2733b240bfea | 62819:d3ff367a16a0 |
|---|---|
67 end; |
67 end; |
68 |
68 |
69 |
69 |
70 (* toplevel pretty printing *) |
70 (* toplevel pretty printing *) |
71 |
71 |
72 val _ = PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => pretty (value var, depth)); |
72 val _ = ML_system_pp (fn depth => fn pretty => fn var => pretty (value var, depth)); |
73 |
73 |
74 end; |
74 end; |