# HG changeset patch
# User blanchet
# Date 1347443271 -7200
# Node ID 82452dc63ed55384a57066cb09d2d2999075a56e
# Parent  a1c10b46fecd0e31f7d05cd4778dd31976b41eb1
desambiguate grammar (e.g. for Nil's mixfix ("[]"))

diff -r a1c10b46fecd -r 82452dc63ed5 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 11:39:05 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 11:47:51 2012 +0200
@@ -704,10 +704,11 @@
 
 val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
 
-val parse_opt_binding_colon = Scan.optional (Parse.binding --| @{keyword ":"}) no_binder
+val parse_binding_colon = Parse.binding --| @{keyword ":"};
+val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binder;
 
 val parse_ctr_arg =
-  @{keyword "("} |-- parse_opt_binding_colon -- Parse.typ --| @{keyword ")"} ||
+  @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
   (Parse.typ >> pair no_binder);
 
 val parse_defaults =