# HG changeset patch
# User huffman
# Date 1242955399 25200
# Node ID bcacfd816d2826e10c57b9479f92f9058db4fa73
# Parent  0aa6afd229d372a6a6a865b5e99b5153638b9379
make type Domain_Library.arg abstract

diff -r 0aa6afd229d3 -r bcacfd816d28 src/HOLCF/Tools/domain/domain_extender.ML
--- a/src/HOLCF/Tools/domain/domain_extender.ML	Wed May 20 13:18:14 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_extender.ML	Thu May 21 18:23:19 2009 -0700
@@ -122,7 +122,7 @@
       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
     fun one_con (con,args,mx) =
 	((Syntax.const_name mx (Binding.name_of con)),
-	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
+	 ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy,
 					find_index_eq tp dts,
 					DatatypeAux.dtyp_of_typ new_dts tp),
 					Option.map Binding.name_of sel,vn))
diff -r 0aa6afd229d3 -r bcacfd816d28 src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Wed May 20 13:18:14 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Thu May 21 18:23:19 2009 -0700
@@ -89,7 +89,9 @@
   val mk_return : term -> term;
   val cproj : term -> 'a list -> int -> term;
   val list_ccomb : term * term list -> term;
+(*
   val con_app : string -> ('a * 'b * string) list -> term;
+*)
   val con_app2 : string -> ('a -> term) -> 'a list -> term;
   val proj : term -> 'a list -> int -> term;
   val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a;
@@ -123,9 +125,10 @@
   val mk_All : string * term -> term;
 
   (* Domain specifications *)
-  type arg = (bool * int * DatatypeAux.dtyp) * string option * string;
+  eqtype arg;
   type cons = string * arg list;
   type eq = (string * typ list) * cons list;
+  val mk_arg : (bool * int * DatatypeAux.dtyp) * string option * string -> arg;
   val is_lazy : arg -> bool;
   val rec_of : arg -> int;
   val sel_of : arg -> string option;
@@ -142,6 +145,8 @@
   val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
   val idx_name : 'a list -> string -> int -> string;
   val app_rec_arg : (int -> term) -> arg -> term;
+  val con_app : string -> arg list -> term;
+
 
   (* Name mangling *)
   val strip_esc : string -> string;
@@ -211,6 +216,7 @@
    typ list) *		(* arguments of abstracted type *)
   cons list;		(* represented type, as a constructor list *)
 
+val mk_arg = I;
 fun rec_of arg  = second (first arg);
 fun is_lazy arg = first (first arg);
 val sel_of    =       second;