| changeset 62819 | d3ff367a16a0 |
| parent 62663 | bea354f6ff21 |
| child 63003 | bf5fcc65586b |
--- a/src/Pure/General/binding.ML Sat Apr 02 20:33:34 2016 +0200 +++ b/src/Pure/General/binding.ML Sat Apr 02 21:10:07 2016 +0200 @@ -154,7 +154,7 @@ val print = Pretty.unformatted_string_of o pretty; -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none); +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none); (* check *)