# HG changeset patch
# User wenzelm
# Date 1369049385 -7200
# Node ID 291bb1f4af295e2efce7513b7308b67c083b3373
# Parent  788b27dfaefaaac86d8eb18a818fc6ca0f51ad83
tuned signature;

diff -r 788b27dfaefa -r 291bb1f4af29 src/HOL/BNF/Tools/bnf_util.ML
--- 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
diff -r 788b27dfaefa -r 291bb1f4af29 src/Tools/Code/code_printer.ML
--- 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