# HG changeset patch
# User berghofe
# Date 1226335045 -3600
# Node ID 71c946ce7eb91bd3d2a96fae4f188dc02aee9b9f
# Parent  cfd169f1dae2d173f8387669c7b41b2b769ab705
Streamlined functions for accessing information about atoms.

diff -r cfd169f1dae2 -r 71c946ce7eb9 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Mon Nov 10 17:34:26 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Nov 10 17:37:25 2008 +0100
@@ -294,9 +294,10 @@
       addsimprocs [mk_perm_bool_simproc ["Fun.id"],
         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     val fresh_star_bij = PureThy.get_thms thy "fresh_star_bij";
-    val pt_insts = map (NominalAtoms.the_atom_info thy #> #pt_inst) atoms;
-    val at_insts = map (NominalAtoms.the_atom_info thy #> #at_inst) atoms;
-    val dj_thms = maps (NominalAtoms.the_atom_info thy #> #dj_thms) atoms;
+    val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
+    val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
+    val dj_thms = maps (fn a =>
+      map (NominalAtoms.dj_thm_of thy a) (atoms \ a)) atoms;
     val finite_ineq = map2 (fn th => fn th' => th' RS (th RS
       @{thm pt_set_finite_ineq})) pt_insts at_insts;
     val perm_set_forget =