diff -r b7b80d5640bb -r 780b7a2c50b6 Nominal/nominal_mutual.ML
--- a/Nominal/nominal_mutual.ML	Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_mutual.ML	Sun Dec 15 15:14:40 2013 +1100
@@ -335,12 +335,12 @@
         [thm] => thm
           |> Drule.gen_all 
           |> Thm.permute_prems 0 1
-          |> (fn thm => atomize_rule (length (prems_of thm) - 1) thm)
+          |> (fn thm => atomize_rule ctxt' (length (prems_of thm) - 1) thm)
       | thms => thms
           |> map Drule.gen_all 
           |> map (Rule_Cases.add_consumes 1)
           |> snd o Rule_Cases.strict_mutual_rule ctxt'
-          |> atomize_concl
+          |> atomize_concl ctxt'
 
     fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac
   in