src/HOLCF/domain/theorems.ML
changeset 2267 b2326aefecbc
parent 2033 639de962ded4
child 2276 3eb9a113029e
     1.1 --- a/src/HOLCF/domain/theorems.ML	Thu Nov 28 10:44:24 1996 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Thu Nov 28 10:50:43 1996 +0100
     1.3 @@ -275,9 +275,10 @@
     1.4                        @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
     1.5                        @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
     1.6      fun distinct (con1,args1) (con2,args2) =
     1.7 -        let val arg1 = (con1, args1);
     1.8 -            val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg)
     1.9 -                        (args2~~variantlist(map vname args2,map vname args1))));
    1.10 +        let val arg1 = (con1, args1)
    1.11 +            val arg2 = (con2,
    1.12 +			ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
    1.13 +                        (args2, variantlist(map vname args2,map vname args1)))
    1.14          in [dist arg1 arg2, dist arg2 arg1] end;
    1.15      fun distincts []      = []
    1.16      |   distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
    1.17 @@ -291,8 +292,9 @@
    1.18          if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
    1.19                                          [eq1, eq2] end;
    1.20      fun distincts []      = []
    1.21 -    |   distincts ((c,leqs)::cs) = flat(map (distinct c) ((map fst cs)~~leqs)) @
    1.22 -                                   distincts cs;
    1.23 +    |   distincts ((c,leqs)::cs) = List_.concat
    1.24 +	            (ListPair.map (distinct c) ((map #1 cs),leqs)) @
    1.25 +		    distincts cs;
    1.26      in distincts (cons~~distincts_le) end;
    1.27  
    1.28  local 
    1.29 @@ -302,7 +304,8 @@
    1.30                  in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
    1.31                        lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs),
    1.32                              mk_trp (foldr' mk_conj 
    1.33 -                                (map rel (map %# largs ~~ map %# rargs)))))) end;
    1.34 +                                (ListPair.map rel
    1.35 +				 (map %# largs, map %# rargs)))))) end;
    1.36    val cons' = filter (fn (_,args) => args<>[]) cons;
    1.37  in
    1.38  val inverts = map (fn (con,args) =>