# HG changeset patch
# User wenzelm
# Date 1466498489 -7200
# Node ID d98164344ec19d0306eb787d9b5f655efc9d5899
# Parent  83a91a73fcb551bcf6fdaa8887a11d4d866cea40
tuned;

diff -r 83a91a73fcb5 -r d98164344ec1 src/Pure/General/binding.ML
--- 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 *)