--- a/src/Pure/sign.ML Tue Apr 05 13:07:40 2011 +0200
+++ b/src/Pure/sign.ML Tue Apr 05 14:25:18 2011 +0200
@@ -91,25 +91,25 @@
val primitive_classrel: class * class -> theory -> theory
val primitive_arity: arity -> theory -> theory
val add_trfuns:
- (string * (ast list -> ast)) list *
+ (string * (Ast.ast list -> Ast.ast)) list *
(string * (term list -> term)) list *
(string * (term list -> term)) list *
- (string * (ast list -> ast)) list -> theory -> theory
+ (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
val add_trfunsT:
(string * (bool -> typ -> term list -> term)) list -> theory -> theory
val add_advanced_trfuns:
- (string * (Proof.context -> ast list -> ast)) list *
+ (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
(string * (Proof.context -> term list -> term)) list *
(string * (Proof.context -> term list -> term)) list *
- (string * (Proof.context -> ast list -> ast)) list -> theory -> theory
+ (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
val add_advanced_trfunsT:
(string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
val add_tokentrfuns:
(string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
-> theory -> theory
- val add_trrules: ast Syntax.trrule list -> theory -> theory
- val del_trrules: ast Syntax.trrule list -> theory -> theory
+ val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
+ val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
val new_group: theory -> theory
val reset_group: theory -> theory
val add_path: string -> theory -> theory