--- a/src/Pure/ROOT.ML Fri Aug 22 11:31:19 2014 +0200
+++ b/src/Pure/ROOT.ML Fri Aug 22 12:05:47 2014 +0200
@@ -343,7 +343,7 @@
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
toplevel_pp ["Position", "T"] "Pretty.position";
-toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print";
+toplevel_pp ["Binding", "binding"] "Binding.pp";
toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";