# HG changeset patch
# User urbanc
# Date 1170951742 -3600
# Node ID 85b065601f4558ac252203b8099373aafac98a86
# Parent  bbc76be6efb49e0643910eb0a909c536efc688b3
added get-functions

diff -r bbc76be6efb4 -r 85b065601f45 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Wed Feb 07 18:12:58 2007 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Thu Feb 08 17:22:22 2007 +0100
@@ -16,6 +16,10 @@
   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;
@@ -57,6 +61,9 @@
 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));