# HG changeset patch
# User wenzelm
# Date 850495062 -3600
# Node ID 73d1435aa729b4350b5f50fb803114ac57b4b57e
# Parent  d360b395766ebe46e4ef50a3e2d6f0e38e07c720
added typed print translations;

diff -r d360b395766e -r 73d1435aa729 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Fri Dec 13 17:37:11 1996 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Fri Dec 13 17:37:42 1996 +0100
@@ -337,6 +337,7 @@
   " val parse_ast_translation = [];\n\
   \ val parse_translation = [];\n\
   \ val print_translation = [];\n\
+  \ val typed_print_translation = [];\n\
   \ val print_ast_translation = [];";
 
 val trfun_args =
@@ -480,6 +481,7 @@
         \\n\
         \|> add_trfuns\n"
         ^ trfun_args ^ "\n\
+        \|> add_trfunsT typed_print_translation \n\
         \\n"
         ^ extxt ^ "\n\
         \\n\
diff -r d360b395766e -r 73d1435aa729 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Dec 13 17:37:11 1996 +0100
+++ b/src/Pure/sign.ML	Fri Dec 13 17:37:42 1996 +0100
@@ -58,6 +58,8 @@
     (string * (term list -> term)) list *
     (string * (term list -> term)) list *
     (string * (ast list -> ast)) list -> sg -> sg
+  val add_trfunsT:
+    (string * (typ -> term list -> term)) list -> sg -> sg
   val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
   val add_trrules_i: ast Syntax.trrule list -> sg -> sg
   val add_name: string -> sg -> sg
@@ -549,6 +551,7 @@
 val add_modesyntax   = extend_sign ext_modesyntax "#";
 val add_modesyntax_i = extend_sign ext_modesyntax_i "#";
 val add_trfuns       = extend_sign (ext_syn Syntax.extend_trfuns) "#";
+val add_trfunsT      = extend_sign (ext_syn Syntax.extend_trfunsT) "#";
 val add_trrules      = extend_sign (ext_syn Syntax.extend_trrules) "#";
 val add_trrules_i    = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
 
diff -r d360b395766e -r 73d1435aa729 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Fri Dec 13 17:37:11 1996 +0100
+++ b/src/Pure/theory.ML	Fri Dec 13 17:37:42 1996 +0100
@@ -43,6 +43,8 @@
     (string * (term list -> term)) list *
     (string * (term list -> term)) list *
     (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
+  val add_trfunsT	:
+    (string * (typ -> term list -> term)) list -> theory -> theory
   val add_trrules     : (string * string)Syntax.trrule list -> theory -> theory
   val add_trrules_i	: Syntax.ast Syntax.trrule list -> theory -> theory
   val cert_axm          : Sign.sg -> string * term -> string * term
@@ -146,6 +148,7 @@
 val add_modesyntax   = curry (ext_sg Sign.add_modesyntax);
 val add_modesyntax_i = curry (ext_sg Sign.add_modesyntax_i);
 val add_trfuns       = ext_sg Sign.add_trfuns;
+val add_trfunsT      = ext_sg Sign.add_trfunsT;
 val add_trrules      = ext_sg Sign.add_trrules;
 val add_trrules_i    = ext_sg Sign.add_trrules_i;
 val add_thyname      = ext_sg Sign.add_name;