| changeset 63335 | d98164344ec1 |
| parent 63006 | 89d19aa73081 |
| child 63352 | 4eaf35781b23 |
--- a/src/Pure/General/binding.ML Mon Jun 20 22:31:16 2016 +0200 +++ b/src/Pure/General/binding.ML Tue Jun 21 10:41:29 2016 +0200 @@ -158,7 +158,7 @@ val print = Pretty.unformatted_string_of o pretty; -val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none); +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty o reset_pos); (* check *)