OuterParse.type_args_constrained;
authorwenzelm
Fri, 19 Mar 2010 00:42:17 +0100
changeset 35839 a601da1056b3
parent 35838 c8bd075c4de8
child 35840 01d7c4ba9050
OuterParse.type_args_constrained;
src/HOLCF/Tools/Domain/domain_extender.ML
--- 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 =