src/Pure/General/binding.ML
changeset 62663 bea354f6ff21
parent 62241 a4a1f282bcd5
child 62819 d3ff367a16a0
--- a/src/Pure/General/binding.ML	Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/General/binding.ML	Fri Mar 18 16:26:35 2016 +0100
@@ -35,7 +35,6 @@
   val concealed: binding -> binding
   val pretty: binding -> Pretty.T
   val print: binding -> string
-  val pp: binding -> Pretty.T
   val bad: binding -> string
   val check: binding -> unit
   val name_spec: scope list -> (string * bool) list -> binding ->
@@ -155,7 +154,7 @@
 
 val print = Pretty.unformatted_string_of o pretty;
 
-val pp = pretty o set_pos Position.none;
+val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none);
 
 
 (* check *)
@@ -191,6 +190,7 @@
       andalso error (bad binding);
   in {restriction = restriction, concealed = concealed, spec = if null spec2 then [] else spec} end;
 
+
 end;
 
 type binding = Binding.binding;