thy_syntax.ML

--- a/thy_syntax.ML	Fri Dec 02 16:09:49 1994 +0100
+++ b/thy_syntax.ML	Fri Dec 02 16:13:34 1994 +0100
@@ -139,7 +139,7 @@
   (*parsers*)
   val tvars = type_args >> map (cat "dtVar");
   val typ =
-    tvars -- name >> (cat "dtTyp" o mk_pair o apfst mk_list) ||
+    tvars -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list) ||
     type_var >> cat "dtVar";
   val opt_typs = optional ("(" $$-- list1 typ --$$ ")") [];
   val constructor = name -- opt_typs -- opt_mixfix;