src/Pure/sign.ML
changeset 42247 12fe41a92cd5
parent 42224 578a51fae383
child 42268 01401287c3f7
     1.1 --- a/src/Pure/sign.ML	Wed Apr 06 13:27:59 2011 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Apr 06 13:33:46 2011 +0200
     1.3 @@ -95,15 +95,14 @@
     1.4      (string * (term list -> term)) list *
     1.5      (string * (term list -> term)) list *
     1.6      (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
     1.7 -  val add_trfunsT:
     1.8 -    (string * (bool -> typ -> term list -> term)) list -> theory -> theory
     1.9 +  val add_trfunsT: (string * (typ -> term list -> term)) list -> theory -> theory
    1.10    val add_advanced_trfuns:
    1.11      (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
    1.12      (string * (Proof.context -> term list -> term)) list *
    1.13      (string * (Proof.context -> term list -> term)) list *
    1.14      (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
    1.15    val add_advanced_trfunsT:
    1.16 -    (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
    1.17 +    (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory
    1.18    val add_tokentrfuns:
    1.19      (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
    1.20    val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list