--- a/src/HOL/Nominal/nominal_atoms.ML Wed Jan 11 12:14:25 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Jan 11 12:21:01 2006 +0100
@@ -714,7 +714,6 @@
in List.mapPartial I (map djs_fun (Library.product ak_names ak_names)) end;
(* list of all fs_inst-theorems *)
val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names
- val pt_id = map (fn ak => PureThy.get_thm thy32 (Name ("pt_"^ak^"1"))) ak_names
fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms);
fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms);
@@ -731,8 +730,7 @@
fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms);
in
thy32
- |> PureThy.add_thmss [(("pt_id", pt_id),[])]
- ||>> 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 [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]