src/HOLCF/domain/axioms.ML
changeset 16394 495dbcd4f4c9
parent 16332 25a440fe5f65
child 16778 2162c0de4673
     1.1 --- a/src/HOLCF/domain/axioms.ML	Tue Jun 14 22:19:32 2005 +0200
     1.2 +++ b/src/HOLCF/domain/axioms.ML	Tue Jun 14 23:44:37 2005 +0200
     1.3 @@ -69,11 +69,11 @@
     1.4  	in map mdef cons end;
     1.5  
     1.6    val sel_defs = let
     1.7 -	fun sdef con n arg = (sel_of arg^"_def",%%:(sel_of arg) == 
     1.8 +	fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
     1.9  		 mk_cRep_CFun(%%:(dname^"_when"),map 
    1.10  			(fn (con',args) => if con'<>con then %%:"UU" else
    1.11 -			 foldr /\# (Bound (length args - n)) args) cons));
    1.12 -	in List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end;
    1.13 +			 foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
    1.14 +	in List.mapPartial Id (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
    1.15  
    1.16  
    1.17  (* ----- axiom and definitions concerning induction ------------------------- *)