| changeset 80809 | 4a64fc4d1cde |
| parent 77960 | 1d82061fbb12 |
| child 80875 | 2e33897071b6 |
--- a/src/Pure/General/binding.ML Wed Sep 04 16:21:52 2024 +0200 +++ b/src/Pure/General/binding.ML Thu Sep 05 17:39:45 2024 +0200 @@ -178,7 +178,7 @@ val print = Pretty.unformatted_string_of o pretty; -val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty o reset_pos); +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_ML o pretty o reset_pos); (* check *)