diff -r 499aa989fbad -r 81bc73585eec src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Fri Nov 26 12:03:17 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML	Fri Nov 26 12:03:18 2010 +0100
@@ -349,7 +349,8 @@
 val _ = List.app Keyword.keyword [datatypesK, functionsK];
 
 val parse_datatype =
-  Parse.name --| Parse.$$$ "=" -- ((Parse.string >> (fn "*" => NONE | _ => Scan.fail ()))
+  Parse.name --| Parse.$$$ "=" --
+    (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
     || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
 
 in