parse length-0 enums as well in Nunchaku

--- 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;