src/Pure/sign.ML
changeset 42224 578a51fae383
parent 42204 b3277168c1e7
child 42247 12fe41a92cd5
     1.1 --- a/src/Pure/sign.ML	Tue Apr 05 13:07:40 2011 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Apr 05 14:25:18 2011 +0200
     1.3 @@ -91,25 +91,25 @@
     1.4    val primitive_classrel: class * class -> theory -> theory
     1.5    val primitive_arity: arity -> theory -> theory
     1.6    val add_trfuns:
     1.7 -    (string * (ast list -> ast)) list *
     1.8 +    (string * (Ast.ast list -> Ast.ast)) list *
     1.9      (string * (term list -> term)) list *
    1.10      (string * (term list -> term)) list *
    1.11 -    (string * (ast list -> ast)) list -> theory -> theory
    1.12 +    (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
    1.13    val add_trfunsT:
    1.14      (string * (bool -> typ -> term list -> term)) list -> theory -> theory
    1.15    val add_advanced_trfuns:
    1.16 -    (string * (Proof.context -> ast list -> ast)) list *
    1.17 +    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
    1.18      (string * (Proof.context -> term list -> term)) list *
    1.19      (string * (Proof.context -> term list -> term)) list *
    1.20 -    (string * (Proof.context -> ast list -> ast)) list -> theory -> theory
    1.21 +    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
    1.22    val add_advanced_trfunsT:
    1.23      (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
    1.24    val add_tokentrfuns:
    1.25      (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
    1.26    val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
    1.27      -> theory -> theory
    1.28 -  val add_trrules: ast Syntax.trrule list -> theory -> theory
    1.29 -  val del_trrules: ast Syntax.trrule list -> theory -> theory
    1.30 +  val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
    1.31 +  val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
    1.32    val new_group: theory -> theory
    1.33    val reset_group: theory -> theory
    1.34    val add_path: string -> theory -> theory