1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Dec 13 17:37:11 1996 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Dec 13 17:37:42 1996 +0100
     1.3 @@ -337,6 +337,7 @@
     1.4    " val parse_ast_translation = [];\n\
     1.5    \ val parse_translation = [];\n\
     1.6    \ val print_translation = [];\n\
     1.7 +  \ val typed_print_translation = [];\n\
     1.8    \ val print_ast_translation = [];";
     1.9  
    1.10  val trfun_args =
    1.11 @@ -480,6 +481,7 @@
    1.12          \\n\
    1.13          \|> add_trfuns\n"
    1.14          ^ trfun_args ^ "\n\
    1.15 +        \|> add_trfunsT typed_print_translation \n\
    1.16          \\n"
    1.17          ^ extxt ^ "\n\
    1.18          \\n\

     2.1 --- a/src/Pure/sign.ML	Fri Dec 13 17:37:11 1996 +0100
     2.2 +++ b/src/Pure/sign.ML	Fri Dec 13 17:37:42 1996 +0100
     2.3 @@ -58,6 +58,8 @@
     2.4      (string * (term list -> term)) list *
     2.5      (string * (term list -> term)) list *
     2.6      (string * (ast list -> ast)) list -> sg -> sg
     2.7 +  val add_trfunsT:
     2.8 +    (string * (typ -> term list -> term)) list -> sg -> sg
     2.9    val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
    2.10    val add_trrules_i: ast Syntax.trrule list -> sg -> sg
    2.11    val add_name: string -> sg -> sg
    2.12 @@ -549,6 +551,7 @@
    2.13  val add_modesyntax   = extend_sign ext_modesyntax "#";
    2.14  val add_modesyntax_i = extend_sign ext_modesyntax_i "#";
    2.15  val add_trfuns       = extend_sign (ext_syn Syntax.extend_trfuns) "#";
    2.16 +val add_trfunsT      = extend_sign (ext_syn Syntax.extend_trfunsT) "#";
    2.17  val add_trrules      = extend_sign (ext_syn Syntax.extend_trrules) "#";
    2.18  val add_trrules_i    = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
    2.19  

     3.1 --- a/src/Pure/theory.ML	Fri Dec 13 17:37:11 1996 +0100
     3.2 +++ b/src/Pure/theory.ML	Fri Dec 13 17:37:42 1996 +0100
     3.3 @@ -43,6 +43,8 @@
     3.4      (string * (term list -> term)) list *
     3.5      (string * (term list -> term)) list *
     3.6      (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
     3.7 +  val add_trfunsT	:
     3.8 +    (string * (typ -> term list -> term)) list -> theory -> theory
     3.9    val add_trrules     : (string * string)Syntax.trrule list -> theory -> theory
    3.10    val add_trrules_i	: Syntax.ast Syntax.trrule list -> theory -> theory
    3.11    val cert_axm          : Sign.sg -> string * term -> string * term
    3.12 @@ -146,6 +148,7 @@
    3.13  val add_modesyntax   = curry (ext_sg Sign.add_modesyntax);
    3.14  val add_modesyntax_i = curry (ext_sg Sign.add_modesyntax_i);
    3.15  val add_trfuns       = ext_sg Sign.add_trfuns;
    3.16 +val add_trfunsT      = ext_sg Sign.add_trfunsT;
    3.17  val add_trrules      = ext_sg Sign.add_trrules;
    3.18  val add_trrules_i    = ext_sg Sign.add_trrules_i;
    3.19  val add_thyname      = ext_sg Sign.add_name;