# HG changeset patch
# User blanchet
# Date 1504821751 -7200
# Node ID a62c0c83feba57d55e7b8b904b86c7f6d92b88db
# Parent  4145169ae609d20c4243032f0aba15c990f97760
parse length-0 enums as well in Nunchaku

diff -r 4145169ae609 -r a62c0c83feba src/HOL/Tools/Nunchaku/nunchaku_model.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_model.ML	Fri Sep 08 00:02:30 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_model.ML	Fri Sep 08 00:02:31 2017 +0200
@@ -177,9 +177,11 @@
     toks o String.explode
   end;
 
-fun parse_enum sep scan = scan ::: Scan.repeat (sep |-- scan);
+fun parse_enum sep scan =
+  Scan.optional (scan ::: Scan.repeat (sep |-- scan)) [];
 
-fun parse_tok tok = Scan.one (curry (op =) tok);
+fun parse_tok tok =
+  Scan.one (curry (op =) tok);
 
 val parse_ident = Scan.some (try (fn Ident id => id));
 val parse_id = parse_tok o Ident;