diff -r f2f611daf480 -r c670a849af65 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Thu Aug 12 21:29:35 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sat Aug 14 16:54:41 2010 +0800
@@ -55,6 +55,9 @@
   (* transformations of premises in inductions *)
   val transform_prem1: Proof.context -> string list -> thm -> thm
   val transform_prem2: Proof.context -> string list -> thm -> thm
+
+  (* transformation into the object logic *)
+  val atomize: thm -> thm
 end
 
 
@@ -256,6 +259,9 @@
   map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm
 
 
+(* transformes a theorem into one of the object logic *)
+val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
+
 
 end (* structure *)