src/Pure/Syntax/lexicon.ML

--- a/src/Pure/Syntax/lexicon.ML	Sun Dec 28 22:10:09 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Mon Dec 29 15:38:59 2014 +0100
@@ -66,6 +66,7 @@
   val is_marked: string -> bool
   val dummy_type: term
   val fun_type: term
+  val pp_lexicon: Scan.lexicon -> Pretty.T
 end;
 
 structure Lexicon: LEXICON =
@@ -451,4 +452,10 @@
 val dummy_type = Syntax.const (mark_type "dummy");
 val fun_type = Syntax.const (mark_type "fun");
 
+
+(* toplevel pretty printing *)
+
+val pp_lexicon =
+  Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon;
+
 end;