src/Pure/sign.ML
changeset 42268 01401287c3f7
parent 42247 12fe41a92cd5
child 42284 326f57825e1a
     1.1 --- a/src/Pure/sign.ML	Thu Apr 07 17:52:44 2011 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Apr 07 18:24:59 2011 +0200
     1.3 @@ -103,10 +103,6 @@
     1.4      (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
     1.5    val add_advanced_trfunsT:
     1.6      (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory
     1.7 -  val add_tokentrfuns:
     1.8 -    (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
     1.9 -  val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
    1.10 -    -> theory -> theory
    1.11    val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
    1.12    val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
    1.13    val new_group: theory -> theory
    1.14 @@ -488,9 +484,6 @@
    1.15  
    1.16  end;
    1.17  
    1.18 -val add_tokentrfuns = map_syn o Syntax.extend_tokentrfuns;
    1.19 -fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
    1.20 -
    1.21  
    1.22  (* translation rules *)
    1.23