--- a/src/Pure/Syntax/lexicon.ML Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Syntax/lexicon.ML Fri Mar 18 16:26:35 2016 +0100
@@ -66,7 +66,6 @@
val is_marked: string -> bool
val dummy_type: term
val fun_type: term
- val pp_lexicon: Scan.lexicon -> Pretty.T
end;
structure Lexicon: LEXICON =
@@ -455,7 +454,8 @@
(* toplevel pretty printing *)
-val pp_lexicon =
- Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon;
+val _ =
+ PolyML.addPrettyPrinter (fn _ => fn _ =>
+ Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
end;