src/HOLCF/Tools/Domain/domain_syntax.ML

           a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
       fun mat (con,args,mx) =
           (mat_name_ con,
            mk_matT(dtype, map third args, freetvar "t" 1),
            Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
-      fun sel1 (_,sel,typ) =
-          Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
-      fun sel (con,args,mx) = map_filter sel1 args;
       fun mk_patT (a,b)     = a ->> mk_maybeT b;
       fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
       fun pat (con,args,mx) =
           (pat_name_ con,
            (mapn pat_arg_typ 1 args)

            Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
     in
     val consts_dis = map dis cons';
     val consts_mat = map mat cons';
     val consts_pat = map pat cons';
-    val consts_sel = maps sel cons';
     end;
 
 (* ----- constants concerning induction ------------------------------------- *)
 
     val const_take   = (dbind "_take"  , HOLogic.natT-->dtype->>dtype, NoSyn);

     end;
     val optional_consts =
         if definitional then [] else [const_rep, const_abs, const_copy];
 
   in (optional_consts @ [const_when] @ 
-      consts_dis @ consts_mat @ consts_pat @ consts_sel @
+      consts_dis @ consts_mat @ consts_pat @
       [const_take, const_finite],
       (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true @ Case_trans)))
   end; (* let *)
 
 (* ----- putting all the syntax stuff together ------------------------------ *)