# HG changeset patch # User wenzelm # Date 878726478 -3600 # Node ID ffb0c9670597e9a726a49801320318389f98c5cb # Parent 873489c611fccd604d32a1c83e3a8d292683cb96 adapted extend_trfunsT; diff -r 873489c611fc -r ffb0c9670597 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Wed Nov 05 11:40:51 1997 +0100 +++ b/src/Pure/Syntax/syntax.ML Wed Nov 05 11:41:18 1997 +0100 @@ -36,7 +36,7 @@ (string * (term list -> term)) list * (string * (term list -> term)) list * (string * (ast list -> ast)) list -> syntax - val extend_trfunsT: syntax -> (string * (typ -> term list -> term)) list -> syntax + val extend_trfunsT: syntax -> (string * (bool -> typ -> term list -> term)) list -> syntax val extend_tokentrfuns: syntax -> (string * string * (string -> string * int)) list -> syntax val extend_trrules: syntax -> (string * string) trrule list -> syntax val extend_trrules_i: syntax -> ast trrule list -> syntax @@ -169,7 +169,7 @@ parse_ast_trtab: ast trtab, parse_ruletab: ruletab, parse_trtab: term trtab, - print_trtab: ((typ -> term list -> term) * stamp) Symtab.table, + print_trtab: ((bool -> typ -> term list -> term) * stamp) Symtab.table, print_ruletab: ruletab, print_ast_trtab: ast trtab, tokentrtab: (string * (string * ((string -> string * int) * stamp)) list) list,