# HG changeset patch
# User urbanc
# Date 1136978461 -3600
# Node ID 3930a060d71b9a80a702d5a6ef0068729aaca1df
# Parent  0cb5a8f501aa0bb99c2e0e9798093a16675300ab
rolled back the last addition since these lemmas were already
in the simpset.

diff -r 0cb5a8f501aa -r 3930a060d71b src/HOL/Nominal/nominal_atoms.ML
--- 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]),[])]