--- a/src/HOL/BNF/Tools/bnf_util.ML Mon May 20 13:07:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Mon May 20 13:29:45 2013 +0200
@@ -167,9 +167,9 @@
val standard_binding: binding
val equal_binding: binding
- val parse_binding: Token.T list -> binding * Token.T list
- val parse_binding_colon: Token.T list -> binding * Token.T list
- val parse_opt_binding_colon: Token.T list -> binding * Token.T list
+ val parse_binding: binding parser
+ val parse_binding_colon: binding parser
+ val parse_opt_binding_colon: binding parser
val typedef: binding * (string * sort) list * mixfix -> term ->
(binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
--- a/src/Tools/Code/code_printer.ML Mon May 20 13:07:31 2013 +0200
+++ b/src/Tools/Code/code_printer.ML Mon May 20 13:29:45 2013 +0200
@@ -101,8 +101,8 @@
| Complex_const_syntax of activated_complex_const_syntax
type tyco_syntax
val requires_args: const_syntax -> int
- val parse_const_syntax: Token.T list -> const_syntax * Token.T list
- val parse_tyco_syntax: Token.T list -> tyco_syntax * Token.T list
+ val parse_const_syntax: const_syntax parser
+ val parse_tyco_syntax: tyco_syntax parser
val plain_const_syntax: string -> const_syntax
val simple_const_syntax: simple_const_syntax -> const_syntax
val complex_const_syntax: complex_const_syntax -> const_syntax