--- a/src/Pure/Syntax/syntax.ML Sun Jul 08 19:52:10 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML Mon Jul 09 11:44:20 2007 +0200
@@ -55,7 +55,7 @@
(string * ((Proof.context -> term list -> term) * stamp)) list *
(string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
(string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
- val extend_tokentrfuns: (string * string * (string -> string * int)) list -> syntax -> syntax
+ val extend_tokentrfuns: (string * string * (string -> output * int)) list -> syntax -> syntax
val remove_const_gram: (string -> bool) ->
mode -> (string * typ * mixfix) list -> syntax -> syntax
val extend_trrules: Proof.context -> (string -> bool) -> syntax ->
@@ -183,7 +183,7 @@
print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
print_ruletab: ruletab,
print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
- tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,
+ tokentrtab: (string * (string * ((string -> output * int) * stamp)) list) list,
prtabs: Printer.prtabs} * stamp;
fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;