diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_library.ML	Sun Dec 15 15:14:40 2013 +1100
@@ -99,9 +99,9 @@
   val transform_prem2: Proof.context -> string list -> thm -> thm
 
   (* transformation into the object logic *)
-  val atomize: thm -> thm
-  val atomize_rule: int -> thm -> thm 
-  val atomize_concl: thm -> thm
+  val atomize: Proof.context -> thm -> thm
+  val atomize_rule: Proof.context -> int -> thm -> thm 
+  val atomize_concl: Proof.context -> thm -> thm
 
   (* applies a tactic to a formula composed of conjunctions *)
   val conj_tac: (int -> tactic) -> int -> tactic
@@ -492,10 +492,10 @@
 
 
 (* transforms a theorem into one of the object logic *)
-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
+fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars;
+fun atomize_rule ctxt i thm =
+  Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm
+fun atomize_concl ctxt thm = atomize_rule ctxt (length (prems_of thm)) thm
 
 
 (* applies a tactic to a formula composed of conjunctions *)