# HG changeset patch
# User blanchet
# Date 1346422026 -7200
# Node ID 1a7b9e4c3153b527fe3181c7f4f95326ec7a4c71
# Parent  b73a74d52aa0032f274bdd355bde0e3ae21ffe3c
made parser a bit more flexible

diff -r b73a74d52aa0 -r 1a7b9e4c3153 src/HOL/Codatatype/Tools/bnf_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 16:07:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 16:07:06 2012 +0200
@@ -56,7 +56,7 @@
   | Free (s, _) => s
   | _ => error "Cannot extract name of constructor";
 
-fun prepare_sugar prep_term (((raw_ctrs, raw_caseof), raw_disc_names), raw_sel_namess)
+fun prepare_sugar prep_term ((raw_ctrs, raw_caseof), (raw_disc_names, raw_sel_namess))
   no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
@@ -403,7 +403,9 @@
     (goals, after_qed, lthy')
   end;
 
-val parse_binding_list = Parse.$$$ "[" |--  Parse.list Parse.binding --| Parse.$$$ "]";
+val parse_bindings = Parse.$$$ "[" |--  Parse.list Parse.binding --| Parse.$$$ "]";
+
+val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]";
 
 val bnf_sugar_cmd = (fn (goalss, after_qed, lthy) =>
   Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo
@@ -412,7 +414,7 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "bnf_sugar"} "adds sugar on top of a BNF"
     (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term --
-      parse_binding_list -- (Parse.$$$ "[" |-- Parse.list parse_binding_list --| Parse.$$$ "]"))
-      >> bnf_sugar_cmd);
+      Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], []))
+     >> bnf_sugar_cmd);
 
 end;