doc-src/IsarRef/Thy/document/Inner_Syntax.tex
changeset 43122 12fe41a92cd5
parent 41495 d797baa3d57c
child 43151 6da43a5018e2
     1.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Apr 06 13:27:59 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Apr 06 13:33:46 2011 +0200
     1.3 @@ -824,8 +824,7 @@
     1.4  val parse_ast_translation   : (string * (ast list -> ast)) list
     1.5  val parse_translation       : (string * (term list -> term)) list
     1.6  val print_translation       : (string * (term list -> term)) list
     1.7 -val typed_print_translation :
     1.8 -  (string * (bool -> typ -> term list -> term)) list
     1.9 +val typed_print_translation : (string * (typ -> term list -> term)) list
    1.10  val print_ast_translation   : (string * (ast list -> ast)) list
    1.11  \end{ttbox}
    1.12  
    1.13 @@ -847,7 +846,7 @@
    1.14  val print_translation:
    1.15    (string * (Proof.context -> term list -> term)) list
    1.16  val typed_print_translation:
    1.17 -  (string * (Proof.context -> bool -> typ -> term list -> term)) list
    1.18 +  (string * (Proof.context -> typ -> term list -> term)) list
    1.19  val print_ast_translation:
    1.20    (string * (Proof.context -> ast list -> ast)) list
    1.21  \end{ttbox}%