src/HOLCF/Tools/Domain/domain_library.ML
changeset 35521 47eec4da124a
parent 35519 abf45a91d24d
child 35522 f9714c7c0837
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 15:46:23 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 15:53:07 2010 -0800
@@ -93,7 +93,7 @@
 
       (* Domain specifications *)
       eqtype arg;
-  type cons = string * mixfix * arg list;
+  type cons = string * arg list;
   type eq = (string * typ list) * cons list;
   val mk_arg : (bool * Datatype.dtyp) * string -> arg;
   val is_lazy : arg -> bool;
@@ -189,7 +189,6 @@
 
 type cons =
      string *         (* operator name of constr *)
-     mixfix *         (* mixfix syntax of constructor *)
      arg list;        (* argument list      *)
 
 type eq =
@@ -227,7 +226,7 @@
 fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
 
 fun dtyp_of_arg ((lazy, D), _) = if lazy then mk_uD D else D;
-fun dtyp_of_cons (_, _, args) = big_sprodD (map dtyp_of_arg args);
+fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
 fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
 
 
@@ -331,8 +330,8 @@
                      else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
 fun when_body cons funarg =
     let
-      fun one_fun n (_,_,[]  ) = /\ "dummy" (funarg(1,n))
-        | one_fun n (_,_,args) = let
+      fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
+        | one_fun n (_,args) = let
             val l2 = length args;
             fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t))
                               else I) (Bound(l2-m));
@@ -342,7 +341,7 @@
                   (args,
                 fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
                ) end;
-    in (if length cons = 1 andalso length(third(hd cons)) <= 1
+    in (if length cons = 1 andalso length(snd (hd cons)) <= 1
         then mk_strictify else I)
          (foldr1 mk_sscase (mapn one_fun 1 cons)) end;