src/HOL/Nominal/nominal_thmdecls.ML

 sig
   val print_data: Proof.context -> unit
   val eqvt_add: attribute
   val eqvt_del: attribute
   val setup: theory -> theory
+  val get_eqvt_thms: theory -> thm list
+  val get_fresh_thms: theory -> thm list
+  val get_bij_thms: theory -> thm list
+  
 
   val NOMINAL_EQVT_DEBUG : bool ref
 end;
 
 structure NominalThmDecls: NOMINAL_THMDECLS =

 (* together, i.e. are of the right "pt_class", so that a stronger version of the     *)
 (* eqality-lemma can be derived. *)
 exception EQVT_FORM;
 
 val print_data = Data.print o Context.Proof;
+val get_eqvt_thms = Context.Theory #> Data.get #> #eqvt;
+val get_fresh_thms = Context.Theory #> Data.get #> #fresh;
+val get_bij_thms = Context.Theory #> Data.get #> #bij;
 
 (* FIXME: should be a function in a library *)
 fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
 
 val perm_bool = thm "perm_bool";