src/HOLCF/Tools/Domain/domain_axioms.ML

       in
         ("copy_def", %%:(dname^"_copy") == /\ "f"
           (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
       end;
 
-(* -- definitions concerning the discriminators and selectors - *)
+(* -- definitions concerning the discriminators - *)
 
     val dis_defs = let
       fun ddef (con,_,_) = (dis_name con ^"_def",%%:(dis_name con) == 
                                               list_ccomb(%%:(dname^"_when"),map 
                                                                               (fn (con',_,args) => (List.foldr /\#

           in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 
                                               list_ccomb(%%:(dname^"_when"), map one_con cons))
           end
       in map pdef cons end;
 
-    val sel_defs = let
-      fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
-                                                            list_ccomb(%%:(dname^"_when"),map 
-                                                                                            (fn (con', _, args) => if con'<>con then UU else
-                                                                                                               List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
-    in map_filter I (maps (fn (con, _, args) => mapn (sdef con) 1 args) cons) end;
-
 
 (* ----- axiom and definitions concerning induction ------------------------- *)
 
     val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
                                          `%x_name === %:x_name));

                    mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
 
   in (dnam,
       (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
       (if definitional then [when_def] else [when_def, copy_def]) @
-      dis_defs @ mat_defs @ pat_defs @ sel_defs @
+      dis_defs @ mat_defs @ pat_defs @
       [take_def, finite_def])
   end; (* let (calc_axioms) *)
 
 
 (* legacy type inference *)