src/Pure/pure_setup.ML
changeset 42381 309ec68442c6
parent 42360 da8817d01e7c
child 43593 11140987d415
--- a/src/Pure/pure_setup.ML	Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/pure_setup.ML	Sun Apr 17 21:42:47 2011 +0200
@@ -22,7 +22,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 quote o Binding.str_of";
+toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print";
 toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
 toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
 toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";