src/HOL/Nominal/nominal_atoms.ML
changeset 25538 58e8ba3b792b
parent 24867 e5b55d7be9bb
child 25557 ea6b11021e79
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Dec 05 14:15:59 2007 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Dec 05 14:16:05 2007 +0100
     1.3 @@ -817,20 +817,20 @@
     1.4  		in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end;
     1.5               (* list of all dj_inst-theorems *)
     1.6               val djs = 
     1.7 -	       let fun djs_fun (ak1,ak2) = 
     1.8 +	       let fun djs_fun ak1 ak2 = 
     1.9  		     if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 (Name ("dj_"^ak2^"_"^ak1)))
    1.10 -	       in List.mapPartial I (map djs_fun (Library.product ak_names ak_names)) end;
    1.11 +	       in map_filter I (map_product djs_fun ak_names ak_names) end;
    1.12               (* list of all fs_inst-theorems *)
    1.13               val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names
    1.14               (* list of all at_inst-theorems *)
    1.15               val fs_axs = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"1"))) ak_names
    1.16  
    1.17 -             fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms);
    1.18 -             fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms);
    1.19 -             fun inst_fs thms = Library.flat (map (fn ti => instR ti fss) thms);
    1.20 -             fun inst_cp thms cps = Library.flat (inst_mult thms cps);
    1.21 +             fun inst_pt thms = maps (fn ti => instR ti pts) thms;
    1.22 +             fun inst_at thms = maps (fn ti => instR ti ats) thms;
    1.23 +             fun inst_fs thms = maps (fn ti => instR ti fss) thms;
    1.24 +             fun inst_cp thms cps = flat (inst_mult thms cps);
    1.25  	     fun inst_pt_at thms = inst_zip ats (inst_pt thms);
    1.26 -             fun inst_dj thms = Library.flat (map (fn ti => instR ti djs) thms);
    1.27 +             fun inst_dj thms = maps (fn ti => instR ti djs) thms;
    1.28  	     fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps;
    1.29               fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms));
    1.30  	     fun inst_pt_pt_at_cp thms =