src/HOLCF/Tools/Domain/domain_library.ML
changeset 35522 f9714c7c0837
parent 35521 47eec4da124a
child 35525 fa231b86cb1e
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 15:53:07 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Tue Mar 02 16:07:48 2010 -0800
@@ -107,8 +107,6 @@
   val nonlazy_rec : arg list -> string list;
   val %# : arg -> term;
   val /\# : arg * term -> term;
-  val when_body : cons list -> (int * int -> term) -> term;
-  val when_funs : 'a list -> string list;
   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;
@@ -326,23 +324,5 @@
   | cont_eta_contract t    = t;
 
 fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
-fun when_funs cons = if length cons = 1 then ["f"] 
-                     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
-            val l2 = length args;
-            fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t))
-                              else I) (Bound(l2-m));
-          in cont_eta_contract
-               (foldr'' 
-                  (fn (a,t) => mk_ssplit (/\# (a,t)))
-                  (args,
-                fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
-               ) end;
-    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;
 
 end; (* struct *)