src/Tools/Code/code_runtime.ML
changeset 40711 81bc73585eec
parent 40422 d425d1ed82af
child 40726 16dcfedc4eb7
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Nov 26 12:03:17 2010 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Nov 26 12:03:18 2010 +0100
     1.3 @@ -349,7 +349,8 @@
     1.4  val _ = List.app Keyword.keyword [datatypesK, functionsK];
     1.5  
     1.6  val parse_datatype =
     1.7 -  Parse.name --| Parse.$$$ "=" -- ((Parse.string >> (fn "*" => NONE | _ => Scan.fail ()))
     1.8 +  Parse.name --| Parse.$$$ "=" --
     1.9 +    (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
    1.10      || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
    1.11  
    1.12  in