--- a/src/HOL/Nominal/nominal_atoms.ML Wed Jan 11 12:11:53 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Jan 11 12:14:25 2006 +0100
@@ -674,6 +674,8 @@
(* instantiations. *)
val (_,thy33) =
let
+
+
(* takes a theorem thm and a list of theorems [t1,..,tn] *)
(* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *)
fun instR thm thms = map (fn ti => ti RS thm) thms;
@@ -712,7 +714,8 @@
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);
fun inst_fs thms = Library.flat (map (fn ti => instR ti fss) thms);
@@ -728,7 +731,8 @@
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 [(("pt_id", pt_id),[])]
+ ||>> 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]),[])]