src/Pure/theory.ML
changeset 2385 73d1435aa729
parent 2359 97b88cafe1e8
child 2693 8300bba275e3
--- 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;