src/HOL/Nominal/nominal_atoms.ML

          |> discrete_pt_inst "List.char" (thm "perm_char_def")
          |> discrete_fs_inst "List.char" (thm "perm_char_def")
          |> discrete_cp_inst "List.char" (thm "perm_char_def")
         end;
 
-
+ 
        (* abbreviations for some lemmas *)
        (*===============================*)
        val abs_fun_pi          = thm "Nominal.abs_fun_pi";
        val abs_fun_pi_ineq     = thm "Nominal.abs_fun_pi_ineq";
        val abs_fun_eq          = thm "Nominal.abs_fun_eq";
+       val abs_fun_eq'         = thm "Nominal.abs_fun_eq'";
        val dj_perm_forget      = thm "Nominal.dj_perm_forget";
        val dj_pp_forget        = thm "Nominal.dj_perm_perm_forget";
        val fresh_iff           = thm "Nominal.fresh_abs_fun_iff";
        val fresh_iff_ineq      = thm "Nominal.fresh_abs_fun_iff_ineq";
        val abs_fun_supp        = thm "Nominal.abs_fun_supp";

 		 in i_pt_pt_at_cp end;
              fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms);
            in
             thy32 
 	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
+            ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])]
             ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])]
             ||>> PureThy.add_thmss 
 	      let val thms1 = inst_pt_at [pt_pi_rev];
 		  val thms2 = inst_pt_at [pt_rev_pi];
               in [(("perm_pi_simp",thms1 @ thms2),[])] end