# HG changeset patch
# User berghofe
# Date 1222433547 -7200
# Node ID 291e7a158e957c0e85f525b344bb29734b64c1d2
# Parent  471a356fdea9324665173277875bb7d129e105ee
Added some more theorems to NominalData.

diff -r 471a356fdea9 -r 291e7a158e95 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Fri Sep 26 14:51:27 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Sep 26 14:52:27 2008 +0200
@@ -11,6 +11,7 @@
   type atom_info
   val get_atom_infos : theory -> atom_info Symtab.table
   val get_atom_info : theory -> string -> atom_info option
+  val the_atom_info : theory -> string -> atom_info
   val atoms_of : theory -> string list
   val mk_permT : typ -> typ
 end
@@ -29,7 +30,10 @@
 type atom_info =
   {pt_class : string,
    fs_class : string,
-   cp_classes : (string * string) list};
+   cp_classes : (string * string) list,
+   at_inst : thm,
+   pt_inst : thm,
+   dj_thms : thm list};
 
 structure NominalData = TheoryDataFun
 (
@@ -40,14 +44,21 @@
   fun merge _ x = Symtab.merge (K true) x;
 );
 
-fun make_atom_info ((pt_class, fs_class), cp_classes) =
+fun make_atom_info (((((pt_class, fs_class), cp_classes), at_inst), pt_inst), dj_thms) =
   {pt_class = pt_class,
    fs_class = fs_class,
-   cp_classes = cp_classes};
+   cp_classes = cp_classes,
+   at_inst = at_inst,
+   pt_inst = pt_inst,
+   dj_thms = dj_thms};
 
 val get_atom_infos = NominalData.get;
 val get_atom_info = Symtab.lookup o NominalData.get;
 
+fun the_atom_info thy name = (case get_atom_info thy name of
+      SOME info => info
+    | NONE => error ("Unknown atom type " ^ quote name));
+
 fun atoms_of thy = map fst (Symtab.dest (NominalData.get thy));
 
 fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
@@ -949,7 +960,9 @@
       NominalData.map (fold Symtab.update (full_ak_names ~~ map make_atom_info
         (pt_ax_classes ~~
          fs_ax_classes ~~
-         map (fn cls => full_ak_names ~~ cls) cp_ax_classes))) thy33
+         map (fn cls => full_ak_names ~~ cls) cp_ax_classes ~~
+         prm_cons_thms ~~ prm_inst_thms ~~
+         map flat dj_thms))) thy33
     end;