# HG changeset patch
# User wenzelm
# Date 857144370 -3600
# Node ID 8300bba275e3784be197c26fe8f0f2ff30839d0f
# Parent  484ec6ca0c506b1413e637c832fb72d8d46265b3
added add_tokentrfuns;

diff -r 484ec6ca0c50 -r 8300bba275e3 src/Pure/sign.ML
--- 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)),
diff -r 484ec6ca0c50 -r 8300bba275e3 src/Pure/theory.ML
--- 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;