src/HOL/Nominal/nominal_atoms.ML
changeset 18651 0cb5a8f501aa
parent 18626 b6596f579e40
child 18652 3930a060d71b
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Jan 11 12:11:53 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Jan 11 12:14:25 2006 +0100
     1.3 @@ -674,6 +674,8 @@
     1.4         (* instantiations.                                                 *)
     1.5         val (_,thy33) = 
     1.6  	 let 
     1.7 +             
     1.8 +
     1.9               (* takes a theorem thm and a list of theorems [t1,..,tn]            *)
    1.10               (* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) 
    1.11               fun instR thm thms = map (fn ti => ti RS thm) thms;
    1.12 @@ -712,7 +714,8 @@
    1.13  	       in List.mapPartial I (map djs_fun (Library.product ak_names ak_names)) end;
    1.14               (* list of all fs_inst-theorems *)
    1.15               val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names
    1.16 -
    1.17 +             val pt_id = map (fn ak => PureThy.get_thm thy32 (Name ("pt_"^ak^"1"))) ak_names
    1.18 +              
    1.19               fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms); 
    1.20               fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms);               
    1.21               fun inst_fs thms = Library.flat (map (fn ti => instR ti fss) thms);
    1.22 @@ -728,7 +731,8 @@
    1.23               fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms);
    1.24             in
    1.25              thy32 
    1.26 -	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
    1.27 +	    |>   PureThy.add_thmss [(("pt_id", pt_id),[])]
    1.28 +            ||>> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
    1.29              ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])]
    1.30              ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
    1.31              ||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]