# HG changeset patch
# User wenzelm
# Date 1144529495 -7200
# Node ID 8198a4ffff24d26b437224c4c6845a2340c7027f
# Parent  ae4a225e0c1fd016e2a7a5ff13d6b5513f1e4339
pretty_term: late externing of consts (support authentic syntax);

diff -r ae4a225e0c1f -r 8198a4ffff24 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Apr 08 22:51:33 2006 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat Apr 08 22:51:35 2006 +0200
@@ -74,7 +74,7 @@
   val read_typ: Context.generic -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
     (sort -> sort) -> string -> typ
   val read_sort: Context.generic -> syntax -> string -> sort
-  val pretty_term: Context.generic -> syntax -> bool -> term -> Pretty.T
+  val pretty_term: (string -> xstring) -> Context.generic -> syntax -> bool -> term -> Pretty.T
   val pretty_typ: Context.generic -> syntax -> typ -> Pretty.T
   val pretty_sort: Context.generic -> syntax -> sort -> Pretty.T
   val ambiguity_level: int ref
@@ -501,7 +501,7 @@
       (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast)
   end;
 
-val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast;
+val pretty_term = pretty_t Printer.term_to_ast o Printer.pretty_term_ast;
 fun pretty_typ context syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast context syn false;
 fun pretty_sort context syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast context syn false;