--- a/src/Pure/sign.ML Fri Feb 28 16:38:55 1997 +0100
+++ b/src/Pure/sign.ML Fri Feb 28 16:39:30 1997 +0100
@@ -60,6 +60,8 @@
(string * (ast list -> ast)) list -> sg -> sg
val add_trfunsT:
(string * (typ -> term list -> term)) list -> sg -> sg
+ val add_tokentrfuns:
+ (string * string * (string -> string * int)) 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
@@ -552,6 +554,7 @@
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_tokentrfuns = extend_sign (ext_syn Syntax.extend_tokentrfuns) "#";
val add_trrules = extend_sign (ext_syn Syntax.extend_trrules) "#";
val add_trrules_i = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
@@ -616,6 +619,7 @@
|> add_syntax Syntax.pure_syntax
|> add_modesyntax (("symbols", true), Syntax.pure_sym_syntax)
|> add_trfuns Syntax.pure_trfuns
+ |> add_trfunsT Syntax.pure_trfunsT
|> add_consts
[("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
--- a/src/Pure/theory.ML Fri Feb 28 16:38:55 1997 +0100
+++ b/src/Pure/theory.ML Fri Feb 28 16:39:30 1997 +0100
@@ -45,6 +45,8 @@
(string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
val add_trfunsT :
(string * (typ -> term list -> term)) list -> theory -> theory
+ val add_tokentrfuns:
+ (string * string * (string -> string * int)) 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
@@ -149,6 +151,7 @@
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_tokentrfuns = ext_sg Sign.add_tokentrfuns;
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;