| changeset 46947 | b8c7eb0c2f89 |
| parent 46737 | 09ab89658a5d |
| child 46949 | 94aa7b81bcf6 |
--- a/src/Tools/Code/code_runtime.ML Thu Mar 15 17:45:54 2012 +0100 +++ b/src/Tools/Code/code_runtime.ML Thu Mar 15 19:02:34 2012 +0100 @@ -349,8 +349,6 @@ val fileK = "file"; val andK = "and" -val _ = List.app Keyword.keyword [datatypesK, functionsK]; - val parse_datatype = Parse.name --| Parse.$$$ "=" -- (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))