added add_tokentrfuns;
authorwenzelm
Fri Feb 28 16:39:30 1997 +0100 (1997-02-28)
changeset 26938300bba275e3
parent 2692 484ec6ca0c50
child 2694 b98365c6e869
added add_tokentrfuns;
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/sign.ML	Fri Feb 28 16:38:55 1997 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Feb 28 16:39:30 1997 +0100
     1.3 @@ -60,6 +60,8 @@
     1.4      (string * (ast list -> ast)) list -> sg -> sg
     1.5    val add_trfunsT:
     1.6      (string * (typ -> term list -> term)) list -> sg -> sg
     1.7 +  val add_tokentrfuns:
     1.8 +    (string * string * (string -> string * int)) list -> sg -> sg
     1.9    val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
    1.10    val add_trrules_i: ast Syntax.trrule list -> sg -> sg
    1.11    val add_name: string -> sg -> sg
    1.12 @@ -552,6 +554,7 @@
    1.13  val add_modesyntax_i = extend_sign ext_modesyntax_i "#";
    1.14  val add_trfuns       = extend_sign (ext_syn Syntax.extend_trfuns) "#";
    1.15  val add_trfunsT      = extend_sign (ext_syn Syntax.extend_trfunsT) "#";
    1.16 +val add_tokentrfuns  = extend_sign (ext_syn Syntax.extend_tokentrfuns) "#";
    1.17  val add_trrules      = extend_sign (ext_syn Syntax.extend_trrules) "#";
    1.18  val add_trrules_i    = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
    1.19  
    1.20 @@ -616,6 +619,7 @@
    1.21    |> add_syntax Syntax.pure_syntax
    1.22    |> add_modesyntax (("symbols", true), Syntax.pure_sym_syntax)
    1.23    |> add_trfuns Syntax.pure_trfuns
    1.24 +  |> add_trfunsT Syntax.pure_trfunsT
    1.25    |> add_consts
    1.26     [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
    1.27      ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
     2.1 --- a/src/Pure/theory.ML	Fri Feb 28 16:38:55 1997 +0100
     2.2 +++ b/src/Pure/theory.ML	Fri Feb 28 16:39:30 1997 +0100
     2.3 @@ -45,6 +45,8 @@
     2.4      (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
     2.5    val add_trfunsT	:
     2.6      (string * (typ -> term list -> term)) list -> theory -> theory
     2.7 +  val add_tokentrfuns:
     2.8 +    (string * string * (string -> string * int)) list -> theory -> theory
     2.9    val add_trrules     : (string * string)Syntax.trrule list -> theory -> theory
    2.10    val add_trrules_i	: Syntax.ast Syntax.trrule list -> theory -> theory
    2.11    val cert_axm          : Sign.sg -> string * term -> string * term
    2.12 @@ -149,6 +151,7 @@
    2.13  val add_modesyntax_i = curry (ext_sg Sign.add_modesyntax_i);
    2.14  val add_trfuns       = ext_sg Sign.add_trfuns;
    2.15  val add_trfunsT      = ext_sg Sign.add_trfunsT;
    2.16 +val add_tokentrfuns  = ext_sg Sign.add_tokentrfuns;
    2.17  val add_trrules      = ext_sg Sign.add_trrules;
    2.18  val add_trrules_i    = ext_sg Sign.add_trrules_i;
    2.19  val add_thyname      = ext_sg Sign.add_name;