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;