# HG changeset patch
# User paulson
# Date 849174643 -3600
# Node ID b2326aefecbc7c578c48bc23f66f8fad186d83f1
# Parent  82aef6857c5b5d7a797df385a1002947bd0e9ffe
Replaced map...~~ by ListPair.map
Tried to tidy up the indenting...

diff -r 82aef6857c5b -r b2326aefecbc src/HOLCF/domain/interface.ML
--- a/src/HOLCF/domain/interface.ML	Thu Nov 28 10:44:24 1996 +0100
+++ b/src/HOLCF/domain/interface.ML	Thu Nov 28 10:50:43 1996 +0100
@@ -53,13 +53,15 @@
     val dnames = map fst dtnvs;
     val num = length dnames;
     val comp_dname = implode (separate "_" dnames);
-    val conss' = map (fn (dname,cons'') =>
-      let
-	fun sel n m = upd_second (fn None   => dname^"_sel_"^(string_of_int n)^
-							 "_"^(string_of_int m)
-				  |  Some s => s)
-	fun fill_sels n con = upd_third (mapn (sel n) 1) con;
-      in mapn fill_sels 1 cons'' end) (dnames~~(map snd eqs''));
+    val conss' = ListPair.map 
+	(fn (dname,cons'') =>
+	  let fun sel n m = upd_second 
+			      (fn None   => dname^"_sel_"^(string_of_int n)^
+						 "_"^(string_of_int m)
+				| Some s => s)
+	      fun fill_sels n con = upd_third (mapn (sel n) 1) con;
+	  in mapn fill_sels 1 cons'' end)
+	(dnames, map #2 eqs'');
     val eqs' = dtnvs~~conss';
 
 (* ----- string for calling add_domain -------------------------------------- *)
diff -r 82aef6857c5b -r b2326aefecbc src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Thu Nov 28 10:44:24 1996 +0100
+++ b/src/HOLCF/domain/theorems.ML	Thu Nov 28 10:50:43 1996 +0100
@@ -275,9 +275,10 @@
                       @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
                       @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
     fun distinct (con1,args1) (con2,args2) =
-        let val arg1 = (con1, args1);
-            val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg)
-                        (args2~~variantlist(map vname args2,map vname args1))));
+        let val arg1 = (con1, args1)
+            val arg2 = (con2,
+			ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
+                        (args2, variantlist(map vname args2,map vname args1)))
         in [dist arg1 arg2, dist arg2 arg1] end;
     fun distincts []      = []
     |   distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
@@ -291,8 +292,9 @@
         if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
                                         [eq1, eq2] end;
     fun distincts []      = []
-    |   distincts ((c,leqs)::cs) = flat(map (distinct c) ((map fst cs)~~leqs)) @
-                                   distincts cs;
+    |   distincts ((c,leqs)::cs) = List_.concat
+	            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
+		    distincts cs;
     in distincts (cons~~distincts_le) end;
 
 local 
@@ -302,7 +304,8 @@
                 in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
                       lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs),
                             mk_trp (foldr' mk_conj 
-                                (map rel (map %# largs ~~ map %# rargs)))))) end;
+                                (ListPair.map rel
+				 (map %# largs, map %# rargs)))))) end;
   val cons' = filter (fn (_,args) => args<>[]) cons;
 in
 val inverts = map (fn (con,args) =>