--- a/src/HOLCF/Tools/Domain/domain_extender.ML Fri Mar 19 00:41:34 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Fri Mar 19 00:42:17 2010 +0100
@@ -301,16 +301,8 @@
val cons_decl =
P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
-val type_var' : (string * string option) parser =
- (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort));
-
-val type_args' : (string * string option) list parser =
- type_var' >> single
- || P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")")
- || Scan.succeed [];
-
val domain_decl =
- (type_args' -- P.binding -- P.opt_mixfix) --
+ (P.type_args_constrained -- P.binding -- P.opt_mixfix) --
(P.$$$ "=" |-- P.enum1 "|" cons_decl);
val domains_decl =