1.1 --- a/src/Pure/Syntax/syntax.ML	Thu Mar 02 12:07:20 1995 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Mar 03 11:48:05 1995 +0100
     1.3 @@ -54,9 +54,9 @@
     1.4    val read: syntax -> typ -> string -> term list
     1.5    val read_typ: syntax -> (indexname -> sort) -> string -> typ
     1.6    val simple_read_typ: string -> typ
     1.7 -  val pretty_term: syntax -> term -> Pretty.T
     1.8 +  val pretty_term: bool -> syntax -> term -> Pretty.T
     1.9    val pretty_typ: syntax -> typ -> Pretty.T
    1.10 -  val string_of_term: syntax -> term -> string
    1.11 +  val string_of_term: bool -> syntax -> term -> string
    1.12    val string_of_typ: syntax -> typ -> string
    1.13    val simple_string_of_typ: typ -> string
    1.14    val simple_pprint_typ: typ -> pprint_args -> unit
    1.15 @@ -403,19 +403,20 @@
    1.16  
    1.17  (** pretty terms or typs **)
    1.18  
    1.19 -fun pretty_t t_to_ast pretty_t (syn as Syntax tabs) t =
    1.20 +fun pretty_t t_to_ast pretty_t curried (syn as Syntax tabs) t =
    1.21    let
    1.22      val {print_trtab, print_ruletab, print_ast_trtab, prtab, ...} = tabs;
    1.23      val ast = t_to_ast (lookup_trtab print_trtab) t;
    1.24    in
    1.25 -    pretty_t prtab (lookup_trtab print_ast_trtab)
    1.26 +    pretty_t curried prtab (lookup_trtab print_ast_trtab)
    1.27        (normalize_ast (lookup_ruletab print_ruletab) ast)
    1.28    end;
    1.29  
    1.30  val pretty_term = pretty_t term_to_ast pretty_term_ast;
    1.31 -val pretty_typ = pretty_t typ_to_ast pretty_typ_ast;
    1.32 +val pretty_typ = pretty_t typ_to_ast pretty_typ_ast false;
    1.33  
    1.34 -fun string_of_term syn t = Pretty.string_of (pretty_term syn t);
    1.35 +fun string_of_term curried syn t =
    1.36 +  Pretty.string_of (pretty_term curried syn t);
    1.37  fun string_of_typ syn ty = Pretty.string_of (pretty_typ syn ty);
    1.38  
    1.39  val simple_string_of_typ = string_of_typ type_syn;