diff -r 06e93f257d0e -r 0d1cbc1fe579 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Fri Apr 08 22:50:50 2011 +0200
+++ b/src/Pure/Isar/parse.ML	Fri Apr 08 22:59:52 2011 +0200
@@ -91,6 +91,8 @@
   val prop_group: string parser
   val term: string parser
   val prop: string parser
+  val type_const: string parser
+  val const: string parser
   val literal_fact: string parser
   val propp: (string * string list) parser
   val termp: (string * string list) parser
@@ -327,6 +329,9 @@
 val term = inner_syntax term_group;
 val prop = inner_syntax prop_group;
 
+val type_const = inner_syntax (group "type constructor" xname);
+val const = inner_syntax (group "constant" xname);
+
 val literal_fact = inner_syntax (group "literal fact" alt_string);