diff -r c8acaded1777 -r 4a00077c008f Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/nominal_library.ML	Fri Jul 22 11:37:16 2011 +0100
@@ -64,6 +64,7 @@
   val fold_append: term list -> term
   val mk_conj: term * term -> term
   val fold_conj: term list -> term
+  val fold_conj_balanced: term list -> term 
 
   (* functions for de-Bruijn open terms *)
   val mk_binop_env: typ list -> string -> term * term -> term
@@ -94,6 +95,8 @@
 
   (* transformation into the object logic *)
   val atomize: thm -> thm
+  val atomize_rule: int -> thm -> thm 
+  val atomize_concl: thm -> thm
 
   (* applies a tactic to a formula composed of conjunctions *)
   val conj_tac: (int -> tactic) -> int -> tactic
@@ -249,6 +252,7 @@
   | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2)
 
 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
+fun fold_conj_balanced ts = Balanced_Tree.make HOLogic.mk_conj ts
 
 
 (* functions for de-Bruijn open terms *)
@@ -476,7 +480,12 @@
 
 
 (* transformes a theorem into one of the object logic *)
-val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars
+val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars;
+fun atomize_rule i thm =
+  Conv.fconv_rule (Conv.concl_conv i Object_Logic.atomize) thm
+fun atomize_concl thm = atomize_rule (length (prems_of thm)) thm
+
+
 
 (* applies a tactic to a formula composed of conjunctions *)
 fun conj_tac tac i =